# Teaching Intuitionistic and Classical Propositional Logic Using Isabelle

Jørgen Villadsen Asta Halkjær From DTU Compute - Department of Applied
Mathematics and Computer Science - Technical University of DenmarkSection of
Philosophy and Science Studies, IKH, Roskilde University, Denmark Patrick
Blackburn Section of Philosophy and Science Studies, IKH, Roskilde University,
Denmark

###### Abstract

We describe a natural deduction formalization of intuitionistic and classical
propositional logic in the Isabelle/Pure framework. In contrast to earlier
work, where we explored the pedagogical benefits of using a deep embedding
approach to logical modelling, here we employ a logical framework modelling.
This gives rise to simple and natural teaching examples and we report on the
role it played in teaching our Automated Reasoning course in 2020 and 2021.

##  1 Introduction

We describe a formalization of intuitionistic and classical propositional
logic in the Isabelle/Pure framework [18, 4, 14]. In a few lines of code we
axiomatize our choice of connectives with their natural deduction introduction
and elimination rules. This gives meaning to the (object) logic via the (meta)
Isabelle/Pure framework rather than in potentially ambiguous natural language.
Unlike pen-and-paper proofs that must be manually checked for mistakes,
Isabelle can check automatically, reducing the burden on lecturers and
teaching assistants. As we will see, by decorating the rules with appropriate
attributes, we never have to mention exactly which rule is being applied, as
the context determines it. This results in proofs that are natural to write
and natural to read.

Our work is based on the Pure/Examples by Makarius in the Isabelle sources:

https://isabelle.in.tum.de/dist/library/Pure/Pure-Examples/document.pdf

That document, however, contains few comments and we have polished the
formalization and tested it in class. Our formalization is available online in
various formats:

https://hol.compute.dtu.dk/Pure_I/

We have used our approach in our Automated Reasoning course in 2020 and 2021:

https://kurser.dtu.dk/course/02256

This is an advanced MSc course (about 40 students) with a focus on the natural
deduction proof system, first-order logic, higher-order logic and type theory,
in particular Isabelle/HOL [13].

We call the approach Pure-I (“pure first”) for two reasons:

  * •

We use Isabelle/Pure as a stepping stone towards the default higher-order
logic in Isabelle/HOL

  * •

We can understand the letter "I" both as a reference to the use of Isabelle by
the students (the tools are a series of Isabelle theory files) but also for
Intuitionism since we let the students add the Law of Excluded Middle (LEM) as
the axiom $p\lor\neg p$ when needed for classical reasoning.

We note that Isabelle/HOL is built on classical logic but with a built-in
proof method for intuitionistic logic (_iprover_).

We focus on propositional logic but extensions to first-order logic as well as
higher-order logic are possible. We use the same natural deduction rule names
as in our natural deduction assistant NaDeA [16]. We teach NaDeA first but
this is not a requirement. However, by teaching NaDeA first we can move
quicker through the material as the rules are already familiar to the students
and only the Isabelle setting is new. This would also be possible if the
students had already learned natural deduction in some other way.

Ideally, our students participating in the MSc course have already taken our
advanced BSc course on Logical Systems and Logic Programming (about 80
students):

https://kurser.dtu.dk/course/02156

In practice this is not the case, in particular due to a large intake of
international students, so we start the MSc course with some weeks on
axiomatic systems and/or sequent calculus presented in a different way than in
the BSc course [10, 17].

Figure 1 shows an actual question for the written exam, 27 May 2021, in our
course 02256 Automated Reasoning. The solution has since been added as theorem
_Peirce_ in Fig. 3.

The exam was 2 hours with all aids. 36 students registered and 30 students
passed.

The distribution of the grades is available online:

https://karakterer.dtu.dk/Histogram/1/02256/Summer-2021

In Denmark we use a so-called 7-step-scale, designed to be compatible with the
ECTS grading scale, with A=12, B=10, C=7, D=4, E=02, Fx=00 and F=-3. Two
students were not graded because they did not show up at the exam. The grade
average were between B and C. This is quite a high grade average but not
unusual for advanced courses.

In the next section we provide an overview of our teaching and the present
paper.

Figure 1: Part of an exam question using our formalization.

##  2 Overview of Teaching and Paper

Table 1: Topics in our course along with relevant tasks (parentheses denote
optional tasks).
Topic | Section | Figures | Tasks
---|---|---|---
Logical Frameworks | 3 |  | Study the Isabelle/Pure framework
Axiomatizations | 4 |  | Study the Pure-I formalization
Definitions | 5 |  | Study the derived rules of defined connectives
Examples | 6 | 2 | Study the Figure
|  |  | Do at least a dozen proofs in intuitionistic logic
|  |  | (Port to Isabelle/HOL: replace Pure-I with Main111Main is the Isabelle theory that defines Isabelle/HOL whereas Pure-I is our axiomatization.)
Classical Logic | 7 |  3, 4 | Study the first Figures
|  |  | Do a few proofs in classical logic
|  | (5, 6, 7, 8) | (Do the proofs in the remaining Figures)
Exam preparation | - | 1 | Do at least a handful of proofs.

We explain the following approaches in the following Section 3:

  * •

Deep Embedding

  * •

Shallow Embedding

  * •

Logical Framework

Our use of Pure-I in the course proceeds in the following way. We ask students
to install Isabelle before the course starts:

https://isabelle.in.tum.de/

As preparation, they can download and open Pure-I (see above) or if Isabelle
is not installed, browse the formalization here:

https://hol.compute.dtu.dk/Pure_I/Pure_I.html

We then cover the topics in Table 1, which are described further in the listed
sections and figures. We have also included tasks for the students that are
relevant to understanding the material.

In Section 8 we take a step back and consider the pedagogical benefits of this
approach from a more general perspective, before we conclude in Section 9.

##  3 Logical Frameworks vs. Deep/Shallow Embeddings

In this paper we present a simple and direct way of teaching propositional
logic, namely by “axiomatizing” the Isabelle/Pure system in the most direct
way possible. The pedagogical benefits of this approach are summed up in the
words ‘simple’ and ‘natural’. The object and metalevel deductions mirror each
other clearly — and the way that teachers would typically instruct students to
construct proofs is directly reflected in the code the students learn to write
to prove things in Isabelle (cf. Section 6).

We have used this system as part of a course on automated reasoning taught at
the Technical University of Denmark (DTU); the course aimed to teach both
natural deduction and Isabelle. It is the latest in a line of systems (based
on courses taught at DTU) which explores different ways in which Isabelle can
be used for pedagogical purposes [9, 8, 15, 16]. For example, in the paper
presented at the 2020 edition of ThEdu, we described a formalization of a
simple axiomatization, called W [9], for classical propositional logic. This
formalization was built using a _deep embedding_ of System W in the higher-
order logic of Isabelle/HOL:

  * Deep Embedding The act of representing one language, typically a logic or programming language, with another by modeling expressions in the former as data in the latter.

– Wiktionary, https://en.wiktionary.org/wiki/deep_embedding

Deep embedding is certainly more appropriate when it comes to teaching many
aspects of metatheory — it forces the student to get to grips with what is
involved in formalizing a language _and its semantics_ , and working in this
way opens a natural path to studying such topics as soundness, completeness
and interpolation (and learning how to use Isabelle/HOL to prove such
results). This has certain pedagogical advantages — we argued in the paper
that this approach forces students to consider metatheoretic issues right from
the start. Deep embeddings are good for this purpose: for example, they make
it possible to teach structural induction on the syntax (which is a key
metalogical proof tool) as the object language syntax has a concrete
representation in the metalogic.

Here, however, we want to take a step back from deep embedding. We want a
gentler approach better suited for a first course in logic, especially for
students with less technical backgrounds. Part of the goal is to teach logic
(rather than metalogic) and in particular to teach natural deduction. The
simple logical framework approach used in this paper enables us to directly
“cook up” our Isabelle/Pure formalization from scratch without worrying about
higher-order logic but while still teaching skills that are transferable to
Isabelle/HOL.

We see the chief benefits of this lighter approach as being simplicity and
elegance. This simplicity and elegance traces to two sources: the fact that we
are working with natural deduction and the ease with which such proof rules
can be reflected in Isabelle/Pure.

We start by introducing intuitionistic propositional logic and only afterwards
axiomatize the Law of Excluded Middle (LEM). Intuitionistic propositional
logic is simple in a number of ways. For example, every statement of the form
$\varphi\lor\psi$ is effectively transformable into an intuitionistic proof of
$\varphi$ or an intuitionistic proof of $\psi$. Moreover, intuitionistic
propositional logic is effectively decidable: a finite constructive process
applies uniformly to every formula, and this process will either produce an
intuitionistic proof of the formula or demonstrate that no such proof can
exist. When working in the intuitionistic fragment, our axiomatization
embodies this process. In other words: it directly reflects, in very simple
code, the process of natural deduction proofs.

We then add some complexity by moving to classical propositional logic.
Working with intuitionistic proofs has built familiarity with the system,
preparing the student to handle the more complicated classical proofs where
there is no longer a clear recipe for how to prove a formula. As we will see,
however, the move to classical logic does not require any new techniques and
can therefore easily be explained.

Besides the logical framework approach taken here and the deep embeddings
considered previously [9], there remains a third option to explore:

  * Shallow Embedding The act of representing one logic or language with another by providing a syntactic translation.

– Wiktionary, https://en.wiktionary.org/wiki/shallow_embedding

Shallow embeddings are another approach to formalizing logics, one that is
widely used in the Isabelle community. Moreover, it is an important way of
thinking about many topics in logic in its own right. Modal logic, for
example, can be thought of in terms of Kripke models (a deep embedding
perspective) but some logicians prefer to emphasize the standard translation
of modal logic into first-order logic (a shallow embedding perspective). It
would be interesting to use a shallow embedding of modal logic in Isabelle/HOL
as a teaching tool that emphasised the standard translation perspective on
modal logic. In terms of modal logic and Isabelle/Pure, Dionísio et al. [5]
have successfully used Isabelle/Pure to teach hybrid logic to students in an
approach similar to ours. The students even define their own labelled modal
logic [3] in the end.

To conclude, in both the deep and shallow embedding approaches, we are forced
to grapple with the complexity of Isabelle/HOL as our metalogic. Here, we only
rely on the simple logical framework of Isabelle/Pure. This leaves more room
for our goal: teaching logic using Isabelle.

##  4 Axiomatizations - Pure-I

In our approach we start at the bottom by declaring the type of formulas in
our object logic, namely boolean:

>   * _typedecl_ bool
>
>

We need to link this type with Isabelle’s type of propositions using a so-
called “truth judgment.” This automatically lifts our formulas so we can use
the machinery provided by the Isabelle/Pure framework. The declaration is
simple:

>   * _judgment_ Trueprop  _$\mathord{:}$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ bool  _$\Rightarrow$_ prop
> _$\scriptscriptstyle\,\,\,\rangle$_
> _$($__$\scriptscriptstyle\langle\,\,\,$_
> -_$\scriptscriptstyle\,\,\,\rangle$__$)$_
>
>

We are now ready to axiomatize our first connective:

>   * _axiomatization_ Imp  _$($__infixr_
> _$\scriptscriptstyle\langle\,\,\,$__$\longrightarrow$__$\scriptscriptstyle\,\,\,\rangle$_
> 3 _$)$_
>
>  _where_ Imp-I  _$[$_ intro _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\Longrightarrow$_ q _$)$_
> _$\Longrightarrow$_ p  _$\longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _and_ Imp-E  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_ q
> _$\Longrightarrow$_ p  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>

The first line declares a name, _Imp_ , for our connective and an infix
symbol, __$\longrightarrow$__ , with right associativity and precedence 3. The
next two lines describe the meaning via an introduction and an elimination
rule. Here we see the power of using the Isabelle/Pure framework. Instead of
using annotations, boxes or similar to discharge assumptions, we simply defer
to the meta-logic’s implication, __$\Longrightarrow$__ , to explain our
object-logic’s implication. That is, to prove that _p_ implies _q_ , assume
_p_ at the meta level and prove _q_ , letting the proof assistant handle the
details. The elimination rule, modus ponens, is symmetric and lifts the
object-level implication into the meta-level, letting us prove _q_ from _p_
when we know _p _$\longrightarrow$_ q_.

We consider the axiomatization of disjunction next:

>   * _axiomatization_ Dis  _$($__infixr_
> _$\scriptscriptstyle\langle\,\,\,$__$\vee$__$\scriptscriptstyle\,\,\,\rangle$_
> 4 _$)$_
>
>  _where_ Dis-E  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\vee$_ q  _$\Longrightarrow$_
> _$($_ p  _$\Longrightarrow$_ r _$)$_  _$\Longrightarrow$_  _$($_ q
> _$\Longrightarrow$_ r _$)$_  _$\Longrightarrow$_ r
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _and_ Dis-I1  _$[$_ intro _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_ p  _$\vee$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _and_ Dis-I2  _$[$_ intro _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ q  _$\Longrightarrow$_ p  _$\vee$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>

Again we declare a name, _Dis_ , and an infix symbol, __$\vee$__. This time we
have one elimination rule and two introduction rules. The elimination rule
allows us to conclude _r_ from _p _$\vee$_ q_ if we can prove _r_ from both
_p_ and _q_. Each of _p_ , _q_ and _r_ are meta-variables that can be
instantiated for any formula. The two introduction rules allow us to form a
disjunction when we have proved either side of it. The attributes on the
rules, _intro_ and _elim_ , will allow us to use them without explicit
reference in the proofs later on.

The axiomatization of conjunction uses the same principles as we have already
seen:

>   * _axiomatization_ Con  _$($__infixr_
> _$\scriptscriptstyle\langle\,\,\,$__$\wedge$__$\scriptscriptstyle\,\,\,\rangle$_
> 5 _$)$_
>
>  _where_ Con-I  _$[$_ intro _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_ q
> _$\Longrightarrow$_ p  _$\wedge$_ q _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _and_ Con-E1  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\wedge$_ q  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _and_ Con-E2  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\wedge$_ q  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>

Finally we axiomatize falsity, __$\bot$__ , with just an elimination rule, the
principle of explosion:

>   * _axiomatization_ Falsity
> _$($__$\scriptscriptstyle\langle\,\,\,$__$\bot$__$\scriptscriptstyle\,\,\,\rangle$__$)$_
>
>  _where_ Falsity-E  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$__$\bot$_  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>

Experienced Isabelle users will see that we have used it in a particularly
simple and direct way: we have turned Isabelle into an “instance” of
intuitionistic logic by adding axioms.

##  5 Definitions - Pure-I

Besides axiomatizations we can provide simple definitions that hide an
expression under a name. In this way, we can define the dual of __$\bot$__ , a
symbol, __$\top$__ , that denotes an always true formula:

>   * _definition_ Truth
> _$($__$\scriptscriptstyle\langle\,\,\,$__$\top$__$\scriptscriptstyle\,\,\,\rangle$__$)$_
> _where_  _$\scriptscriptstyle\langle\,\,\,$__$\top$_  _$\equiv$_  _$\bot$_
> _$\longrightarrow$_  _$\bot$__$\scriptscriptstyle\,\,\,\rangle$_
>
>

We can still give a meaning to this, as an introduction rule, so we do not
need to consider the implementation details later. Instead of being part of an
axiomatization, this introduction rule is stated simply as a theorem:

>   * _theorem_ Truth-I  _$[$_ intro _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$__$\top$__$\scriptscriptstyle\,\,\,\rangle$_
>
>  _unfolding_ Truth-def  _.._
>
>

Several concepts are at play here. In the first line we state the name of the
theorem, the attributes and the goal __$\top$__. Next we unfold the
definition, transforming the goal into __$\bot$_ _$\longrightarrow$_
_$\bot$__. The two periods _.._ apply a matching introduction rule for the
connective, in this case _Imp-I_. That reduces the goal to __$\bot$_
_$\Longrightarrow$_ _$\bot$__ , which is discharged automatically.

We define negation in the usual way, as implication of a contradiction:

>   * _definition_ Neg  _$($__$\scriptscriptstyle\langle\,\,\,$__$\neg$_
> -_$\scriptscriptstyle\,\,\,\rangle$_  _$[$_ 6 _$]$_ 6 _$)$_  _where_
> _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ p  _$\equiv$_ p
> _$\longrightarrow$_  _$\bot$__$\scriptscriptstyle\,\,\,\rangle$_
>
>

This brings us to a more interesting theorem and proof: from a formula and its
negation we can prove anything. We start by stating the theorem and unfolding
the definition:

>   * _theorem_ Neg-E  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ p  _$\Longrightarrow$_ p
> _$\Longrightarrow$_ q _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _unfolding_ Neg-def
>
> _proof_  _$-$_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_
> _$\bot$__$\scriptscriptstyle\,\,\,\rangle$_  _and_
> _$\scriptscriptstyle\langle\,\,\,$_ p _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _then_  _have_
> _$\scriptscriptstyle\langle\,\,\,$__$\bot$__$\scriptscriptstyle\,\,\,\rangle$_
> _.._
>
>  _then_  _show_  _$\scriptscriptstyle\langle\,\,\,$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
> _qed_
>
>

The _proof_ command starts the proof and the following hyphen tells Isabelle
not to apply any initial proof rules to transform the goal (further). The
_assume_ command on the next line is implication introduction at the meta-
level: it introduces the two __$\Longrightarrow$__ connectives in the goal.
Since we unfolded the definition of negation, the first assumption is _p
_$\longrightarrow$_ _$\bot$__ , while the second one is _p_ as expected. The
_then_ command makes these two assumptions (or any other just stated fact)
available to the following command, which in this case is _have_. This command
is used to state local results and here we use it to prove __$\bot$__ from the
two assumptions. The two periods  _.._ automatically apply the _Imp-E_ rule to
_p _$\longrightarrow$_  _$\bot$__ and _p_ in the proof context. The _show_ on
the penultimate line states a result like _have_ but also discharges a goal,
in our case _q_. Here the two periods automatically apply the _Falsity-E_
rule. The final _qed_ matches the initial _proof_ and marks the end of the
proof. It only “succeeds” if there are no remaining goals.

We define bi-implication as implication in both directions:

>   * _definition_ Iff  _$($__infixr_
> _$\scriptscriptstyle\langle\,\,\,$__$\longleftrightarrow$__$\scriptscriptstyle\,\,\,\rangle$_
> 3 _$)$_  _where_  _$\scriptscriptstyle\langle\,\,\,$_ p
> _$\longleftrightarrow$_ q  _$\equiv$_  _$($_ p  _$\longrightarrow$_ q _$)$_
> _$\wedge$_  _$($_ q  _$\longrightarrow$_ p
> _$)$__$\scriptscriptstyle\,\,\,\rangle$_
>
>

Again, we want to prove introduction and elimination rules that allow us to
work with the connective without unfolding its definition. We start with the
introduction rule. Given that we can prove _q_ from _p_ and _p_ from _q_ we
seek to prove _p _$\longleftrightarrow$_ q_:

>   * _theorem_ Iff-I  _$[$_ intro _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\Longrightarrow$_ q _$)$_
> _$\Longrightarrow$_  _$($_ q  _$\Longrightarrow$_ p _$)$_
> _$\Longrightarrow$_ p  _$\longleftrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _unfolding_ Iff-def
>
> _proof_  _$-$_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _and_
> _$\scriptscriptstyle\langle\,\,\,$_ q  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _have_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _have_
> _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _and_
> _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _show_
> _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\longrightarrow$_ q _$)$_
> _$\wedge$_  _$($_ q  _$\longrightarrow$_ p
> _$)$__$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
> _qed_
>
>

We have already seen the _proof_ and _assume_ commands, which are used in the
same way here. Instead of using _then_ , we pick out the assumptions one at a
time with _from_ in the next two lines, introducing the object-logic
implication in each direction. The final line combines the two implications
into their conjunction: the definition of bi-implication.

The proofs of the two elimination rules only use techniques we have already
seen, but some other axiomatized rules, making them suitable as exercises:

>   * _theorem_ Iff-E1  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longleftrightarrow$_ q
> _$\Longrightarrow$_ p  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _unfolding_ Iff-def
>
> _proof_  _$-$_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\longrightarrow$_ q
> _$)$_  _$\wedge$_  _$($_ q  _$\longrightarrow$_ p
> _$)$__$\scriptscriptstyle\,\,\,\rangle$_
>
>  _then_  _have_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_
> q _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _then_  _show_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_
> q _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
> _qed_
>
>

>   * _theorem_ Iff-E2  _$[$_ elim _$]$__$\mathord{:}$_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longleftrightarrow$_ q
> _$\Longrightarrow$_ q  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _unfolding_ Iff-def
>
> _proof_  _$-$_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\longrightarrow$_ q
> _$)$_  _$\wedge$_  _$($_ q  _$\longrightarrow$_ p
> _$)$__$\scriptscriptstyle\,\,\,\rangle$_
>
>  _then_  _have_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longrightarrow$_
> p _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _then_  _show_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\Longrightarrow$_
> p _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
> _qed_
>
>

##  6 Selected Teaching Examples

Let us examine some examples. The _proposition_ command is an alternative name
for _theorem_ and we use it for student exercises and examples. There is no
difference to the system, only to the human reader.

>   * _proposition_  _$\scriptscriptstyle\langle\,\,\,$_ p
> _$\longrightarrow$_  _$\neg$_  _$\neg$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
> _proof_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _show_  _$\scriptscriptstyle\langle\,\,\,$__$\neg$_  _$\neg$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _proof_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _and_
> _$\scriptscriptstyle\langle\,\,\,$_ p _$\scriptscriptstyle\,\,\,\rangle$_
> _show_
> _$\scriptscriptstyle\langle\,\,\,$__$\bot$__$\scriptscriptstyle\,\,\,\rangle$_
> _.._
>
>  _qed_
>
> _qed_
>
>

Note the way the Isabelle/Pure code matches the way we would explain to
students how they should go about proving this in natural deduction. It
essentially spells out a constructive process for building the proof tree
required — with the formula being proved if and only if such a proof tree
exists.

In Fig. 2 we see the same example but with explicit rule names like _Imp_I_
and _Neg_I_ (and syntax highlighting as seen by the students). It is always
possible to write explicitly which rule justifies a proof step, either for
clarity or to convince oneself that the implicitly applied rule is the
expected one. In general, however, we prefer to leave such rules implicit, so
the structure of the proof stands out clearly.

Figure 2: A simple teaching example with explicit rule names in Isabelle/Pure.

Here is a proof of modus tollens. Once again, note how Isabelle/Pure tracks
the way a teacher would explain to a beginner how to construct the relevant
proof tree:

>   * _proposition_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p
> _$\longrightarrow$_ q _$)$_  _$\wedge$_  _$\neg$_ q  _$\longrightarrow$_
> _$\neg$_ p _$\scriptscriptstyle\,\,\,\rangle$_
>
> _proof_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\longrightarrow$_ q
> _$)$_  _$\wedge$_  _$\neg$_ q _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _show_  _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _proof_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\longrightarrow$_ q
> _$)$_  _$\wedge$_  _$\neg$_ q _$\scriptscriptstyle\,\,\,\rangle$_  _have_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _and_
> _$\scriptscriptstyle\langle\,\,\,$_ p _$\scriptscriptstyle\,\,\,\rangle$_
> _have_  _$\scriptscriptstyle\langle\,\,\,$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p  _$\longrightarrow$_ q
> _$)$_  _$\wedge$_  _$\neg$_ q _$\scriptscriptstyle\,\,\,\rangle$_  _have_
> _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$__$\neg$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _and_
> _$\scriptscriptstyle\langle\,\,\,$_ q _$\scriptscriptstyle\,\,\,\rangle$_
> _show_
> _$\scriptscriptstyle\langle\,\,\,$__$\bot$__$\scriptscriptstyle\,\,\,\rangle$_
> _.._
>
>  _qed_
>
> _qed_
>
>

Here is a more complex example:

>   * _proposition_  _$\scriptscriptstyle\langle\,\,\,$__$($_ p
> _$\longleftrightarrow$_ q _$)$_  _$\longleftrightarrow$_ q
> _$\longleftrightarrow$_ p _$\scriptscriptstyle\,\,\,\rangle$_
>
> _proof_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longleftrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _show_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longleftrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _proof_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longleftrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _show_
> _$\scriptscriptstyle\langle\,\,\,$_ q  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _next_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longleftrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _show_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _qed_
>
> _next_
>
>  _assume_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longleftrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _show_  _$\scriptscriptstyle\langle\,\,\,$_ p  _$\longleftrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_
>
>  _proof_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longleftrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _show_
> _$\scriptscriptstyle\langle\,\,\,$_ p  _$\Longrightarrow$_ q
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _next_
>
>  _from_  _$\scriptscriptstyle\langle\,\,\,$_ q  _$\longleftrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _show_
> _$\scriptscriptstyle\langle\,\,\,$_ q  _$\Longrightarrow$_ p
> _$\scriptscriptstyle\,\,\,\rangle$_  _.._
>
>  _qed_
>
> _qed_
>
>

Here, we need to prove both directions of the middle bi-implication by
assuming the left-hand side and showing the right and vice versa.
Conceptually, the _next_ command switches to proving the remaining direction.
Technically, it resets the local context, so we cannot use the assumption from
the proof in one direction in the proof of the other direction. With this
command at hand, the proof almost writes itself.

The above example works verbatim in Isabelle/HOL. This makes the skills
obtained by working with this logic directly transferable to the larger
setting of higher-order logic. The syntax is the same and the same rules are
available, making this a stepping stone for proving things in Isabelle/HOL.

##  7 Classical Logic

Imagine we try to prove a formula that does not have a proof in our logic,
e.g. Peirce’s law:

$((p\longrightarrow q)\longrightarrow p)\longrightarrow p$

We can take a stab at it, applying introduction rules for the implications and
so on, but we will never succeed. Like with pen and paper, the system does not
provide any indication that no proof exists, but unlike with pen and paper we
cannot mistakenly think one does by writing down a flawed proof. That specific
formula does hold in classical propositional logic and so we could extend the
axiomatization with the Law of Excluded Middle (LEM) $p\lor\neg p$ to work in
that logic instead. Then we would be able to find a proof.

In Fig. 3 we do so by axiomatizing the Law of Excluded Middle (LEM) on top of
Pure-I. This axiomatization of a simple formula is easy to explain to students
and clearly states an important point in classical logic: for every
proposition, either this proposition or its negation is true. We first derive
a more useful principle _classical_ , named after its counterpart in
Isabelle/HOL. The single period command proves immediate facts like _p
_$\Longrightarrow$_ p_. The _with_ command makes one or more assumptions or
previously established facts available as justification for the following
statement. We use the theorem _classical_ to prove Clavius’s law and Peirce’s
law; we can no longer rely only on two periods as for intuionistic proofs, but
must explicitly invoke a classical principle in the proof.

Figure 3: Axiomatization of the Law of Excluded Middle (LEM) with subsequent
proofs of three other principles in classical logic.

In Fig. 4 we give a wordy proof of the _classical_ theorem from Fig. 3. Here
we use the full name _this_ for the single period proof method and _standard_
for the double period. We also state _LEM_ directly and use _from_ instead of
_with_ to be more explicit. It is often useful for students to work with
variants of the key proofs.

Figure 4: A proof from Fig. 3 with explicit rules.

In Fig. 5 we consider the special NaDeA rule Boole in the Isabelle/Pure
setting. After proving it from _classical_ (and transitively _LEM_), we prove
a variant of double negation elimination using it. Formulas like this can be
used either for demonstration or as student exercises.

Figure 5: A proof of the classical principle Boole used in NaDeA and a
subsequent proof.

In Fig. 6 we consider classical contradiction (_ccontr_ in Isabelle/HOL): if
from __$\neg$_ p_ we can derive falsity, then we can conclude _p_. We have
already proved this as Boole when we recall that we have defined $\neg p\equiv
p\longrightarrow\bot$. We then prove the same formula as in Fig. 5 but stated
using negation.

Figure 6: A classical proof using the principle Boole from NaDeA formulated as
in Isabelle/HOL.

In Fig. 7 we define __$\bot$__ and __$\top$__ in Isabelle/HOL as _False_ and
_True_ , respectively. We then define the Boole rule from the pre-defined
_ccontr_ by unfolding negation similarly to previously. Then we can insert our
proof from Fig. 5 unmodified. This demonstrates how the skills obtained from
working with our formalization in Isabelle/Pure are transferable to the full
Isabelle/HOL.

Figure 7: A proof from Fig. 5 after a few definitions in Isabelle/HOL.

In Fig. 8 we consider classical contradiction (_ccontr_) already available in
Isabelle/HOL by repeating the proof from Fig. 6 in this setting.

Figure 8: A proof from Fig. 6 using the pre-defined _ccontr_ in Isabelle/HOL.

As exercises we offer a number of formulas to be proved in intuitionistic or
classical logic.

##  8 The Role of Proof Assistants

We have already mentioned a number of features of our course which we feel are
pedagogically useful. In this section we want to stand back, take a more
general perspective on our goals, and speculate a little about the future role
of Isabelle/Pure (and other proof assistants) in the teaching of logic and
mathematics.

Intuitionistic logic, perhaps more than any other logic, is interesting both
philosophically and computationally. The key ideas of intuitionism are due to
the Dutch mathematician Luitzen Egbertus Jan Brouwer, and they played a
prominent role in the early 20th century debate on the foundations of
mathematics. Brouwer was opposed to Russell’s logicism (Brouwer viewed logic
as part of mathematics, not as a foundation for it) and also to Hilbert’s
formalism (intuitionistic logic was formalized not by Brouwer himself but by
later followers such as Heyting). Key themes driving Brouwer’s philosophy of
mathematics were the activity of proof, and the construction of mathematical
objects; these were conceived as mental activities of the “creative subject”,
thus Brouwer attempted to side-step Platonism as well (the view that
mathematics is the discovery of truths about some abstract, pre-existing
metaphysical realm). As is well known, variants of Brouwer’s ideas have led to
the developments of new logic(s) and have become a source of inspiration for
later developments in constructive mathematics and program development. For
more background on the technical, conceptual and historical underpinnings of
intuitionism, see [12, 11, 2].

To state simply what we shall spell out in the following paragraphs: we
believe that teaching intuitionistic logic early in a student’s career — and
carefully drawing attention to the differences with classical logic — is
pedagogically useful because it sensitizes students to the nuances of proof.
Moreover, we believe that doing so in the setting of Isabelle/Pure (or indeed,
some other proof assistant) forces students to grapple more deeply with these
distinctions, enables active experimentation, and prepares them for a future
in which technology is likely to play an increasingly important role in logic
and mathematics. Let us now try and explain why.

The constructive nature of intuitionistic proof is partially clarified in the
BHK-interpretation (the Brouwer, Heyting, Kolmogorov interpretation) which
contains clauses like the following:

> A proof of $\varphi\rightarrow\psi$ is any construction which converts any
> proof of $\varphi$ into a proof of $\psi$.

Similarly:

> A negated formula $\neg\varphi$ is proved by giving a construction that
> converts a proof of $\varphi$ into a proof of $\bot$ (where $\bot$ is
> unprovable).

The BHK-interpretation is an intuitive interpretation rather than a formal
one, because it does not make clear what a “construction” (or “converts”)
mean. But it is certainly suggestive. For example, any currently unproved
mathematical statement, such as the Goldbach Conjecture (every even number
greater than two is the sum of two primes) for which we have neither a proof,
nor a proof of its negation, is a counterexample to LEM. Of course, we may
lose some LEM counterexamples over time: Fermat’s Last Theorem used to be such
a counterexample, but it stopped being one around September 1994, when Andrew
Wiles had the crucial insight that lead him to the correct proof. That is,
Brouwer’s view of mathematics emphasizes the dynamic role of creative
construction, and the BHK-interpretation captures some of this. Furthermore,
the words commonly used to describe the BHK-interpretation, like
“construction”, “converts” or “transform” have a computational flavour.
Indeed, one way of thinking about constructions is as programs: a proof of
$\varphi\rightarrow\psi$ is a program that takes a proof of $\varphi$ as input
and outputs a proof of $\psi$. This way of thinking is commonplace nowadays in
various subfields of computer science, such as functional programming, and
lies at the heart of what has become known as the Curry-Howard isomorphism.

The late Michael Dummett, an influential English philosopher, published a
well-known paper in 1975 (see [6], and also [7]) that attached philosophical
significance to intuitionistic logic, but for reasons rather different from
those emphasized by Brouwer and his followers. Brouwer emphasized the role of
the “creative subject” – mathematics was some sort of non-linguistic mental
activity. Dummett, on the other hand, strongly emphasizes the linguistic
elements of mathematics; see [11] for a clear discussion. Dummett emphasizes
that mathematics is a language that is to be used to be understand.
Mathematics is about learning to do certain things – finding square roots,
solving equations, differentiating functions, or proving theorems and
corollaries. Learning the underlying logic of mathematics is all about
learning what we need to do with logical statements — it’s about process — and
the ability to recognize proofs and to appreciate their fine structure is a
key part of this.

And this is the point where we feel the use of proof assistants such as
Isabelle/Pure come in: they open up new research and pedagogical spaces for
this process. Dummett’s paper is now almost half a century old, thus it
precedes the era of interactive technologies which boost human cognitive
capacities. Proof assistants are precisely such a technology: they open up new
ways to explore the mathematical landscape via human-machine interaction. That
is: what strikes us as interesting about Dummett’s work is the emphasis it
places on linguistic/logical explorations underlying mathematics, and the
activity of learning ways of proving. And proof assistants provide a truly
novel way of zooming in on these activities.

Dummett may or may not be right to single out intuitionistic logic as special
— we prefer to think in terms of logics of mathematics. But as a pedagogical
tool, intuitionistic logic is undeniably useful. Teaching intuitionistic
propositional logic early primes students to be aware of the nuances of
mathematical proof. Doing so with the aid of a proof assistant, where they can
actively compare classical and intuitionistic logics, amplifies the insights.
It seems plausible that proof assistants will play an increasingly significant
role in the development of mathematics and logic, turning research in new and
unexpected directions. We should be training students in ways that will help
them explore these new worlds, and our courses can be viewed as simple
experiments in how to do this.

##  9 Concluding Remarks

We have shown how to use Isabelle/Pure as a logical framework for teaching
intuitionistic and classical propositional logic. Instead of teaching each
logic separately, we have shown first how to axiomatize an intuitionistic base
and then how to add classical reasoning on top of it. Along these lines, we
want students to learn a framework for describing natural deduction rules
instead of only learning the rules themselves. We see this approach scaling
from propositional logic to first-order logic and even further to higher-order
logic. By defining each logic in the same logical framework we hope to make
the distinctions between them clear to the students and want to explore this
in future work.

## Acknowledgements

Thanks to Frederik Krogsdal Jacobsen and the anonymous reviewers for comments.

## References

  * [1]
  * [2] Mark van Atten (2020): _Luitzen Egbertus Jan Brouwer_.  In Edward N. Zalta, editor: The Stanford Encyclopedia of Philosophy, Spring 2020 edition, Metaphysics Research Lab, Stanford University.
  * [3] David A. Basin, Seán Matthews & Luca Viganò (1998): _Labelled Modal Logics: Quantifiers_.  Journal of Logic, Language and Information 7(3), pp. 237–263, 10.1023/A:1008278803780.
  * [4] Stefan Berghofer & Makarius Wenzel (2008): _Logic-Free Reasoning in Isabelle/Isar_.  In Serge Autexier, John A. Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki & Freek Wiedijk, editors: Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings, Lecture Notes in Computer Science 5144, Springer, pp. 355–369, 10.1007/978-3-540-85110-3_31.
  * [5] F. Miguel Dionísio, Paula Gouveia & João Marcos (2005): _Defining and using deductive systems with Isabelle_.  Computing, Philosophy, and Cognition, pp. 271–293.
  * [6] Michael Dummett (1975): _The philosophical basis of intuitionistic logic_.  In: Studies in Logic and the Foundations of Mathematics, 80, Elsevier, pp. 5–40.
  * [7] Michael Dummett (2000): _Elements of intuitionism_.  Oxford University Press.
  * [8] Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen (2019): _Teaching a Formalized Logical Calculus_.  In Pedro Quaresma, Walther Neuper & João Marcos, editors: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019, EPTCS 313, pp. 73–92, 10.4204/EPTCS.313.5.
  * [9] Asta Halkjær From, Jørgen Villadsen & Patrick Blackburn (2020): _Isabelle/HOL as a Meta-Language for Teaching Logic_.  In Pedro Quaresma, Walther Neuper & João Marcos, editors: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020, EPTCS 328, pp. 18–34, 10.4204/EPTCS.328.2.
  * [10] Asta Halkjær From (2021): _Soundness and Completeness of an Axiomatic System for First-Order Logic_.  Archive of Formal Proofs.  https://isa-afp.org/entries/FOLAxiomatic.html, Formal proof development.
  * [11] Rosalie Iemhoff (2020): _Intuitionism in the Philosophy of Mathematics_.  In Edward N. Zalta, editor: The Stanford Encyclopedia of Philosophy, Fall 2020 edition, Metaphysics Research Lab, Stanford University.
  * [12] Joan Moschovakis (2021): _Intuitionistic Logic_.  In Edward N. Zalta, editor: The Stanford Encyclopedia of Philosophy, Fall 2021 edition, Metaphysics Research Lab, Stanford University.
  * [13] Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): _Isabelle/HOL — A Proof Assistant for Higher-Order Logic_.  Lecture Notes in Computer Science 2283, Springer, 10.1007/3-540-45949-9.
  * [14] Lawrence C. Paulson (1989): _The Foundation of a Generic Theorem Prover_.  J. Autom. Reason. 5(3), pp. 363–397, 10.1007/BF00248324.
  * [15] Anders Schlichtkrull, Jørgen Villadsen & Andreas Halkjær From (2018): _Students’ Proof Assistant (SPA)_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 7th International Workshop on Theorem proving components for Educational software, THedu@FLoC 2018, Oxford, United Kingdom, 18 july 2018, EPTCS 290, pp. 1–13, 10.4204/EPTCS.290.1.
  * [16] Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2017): _Natural Deduction and the Isabelle Proof Assistant_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017, EPTCS 267, pp. 140–155, 10.4204/EPTCS.267.9.
  * [17] Jørgen Villadsen, Anders Schlichtkrull & Andreas Halkjær From (2018): _A Verified Simple Prover for First-Order Logic_.  In Boris Konev, Josef Urban & Philipp Rümmer, editors: Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR 2018) co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, 19 July 2018, CEUR Workshop Proceedings 2162, CEUR-WS.org, pp. 88–104.  Available at http://ceur-ws.org/Vol-2162/paper-08.pdf.
  * [18] Makarius Wenzel, Lawrence C. Paulson & Tobias Nipkow (2008): _The Isabelle Framework_.  In Otmane A¨t Mohamed, César A. Muñoz & Sofiène Tahar, editors: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, Lecture Notes in Computer Science 5170, Springer, pp. 33–38, 10.1007/978-3-540-71067-7_7.


# Dynamics of a Klein-Gordon Oscillator (KGO) in the Presence of a Cosmic
String in Som–Raychaudhuri Space-Time

Abdelmalek Bouzenada<EMAIL_ADDRESS>;
<EMAIL_ADDRESS>Laboratory of theoretical and applied Physics,
Echahid Cheikh Larbi Tebessi University, Algeria  Abdelmalek Boumali
<EMAIL_ADDRESS>Laboratory of theoretical and applied Physics,
Echahid Cheikh Larbi Tebessi University, Algeria  R. L. L .Vitória
<EMAIL_ADDRESS><EMAIL_ADDRESS>Faculdade de Física,
Universidade Federal do Pará, Av. Augusto Corrêa,
Guamá, Belém, PA 66075-110, Brazil  C. Furtado<EMAIL_ADDRESS>Departamento de Física, Universidade Federal da Paraíba,
Caixa Postal 5008, João Pessoa-PB 58051-900, Brazil

(August 28, 2024)

###### Abstract

This paper explores the dynamics of the Klein-Gordon oscillator in the
presence of a cosmic string in Som Raychaudhuri spacetime. The exact solutions
for the free case and the oscillator case are obtained and discussed. These
solutions reveal the effects of the cosmic string and the spacetime geometry
on the bosonic particles. To illustrate these results, some figures and tables
have been included.

Klein-Gordon oscillator, topological defects, cosmic string, Som–Raychaudhuri
Space-Time.

###### pacs:

04.62.+v; 04.40.−b; 04.20.Gz; 04.20.Jb; 04.20.−q; 03.65.Pm; 03.50.−z;
03.65.Ge; 03.65.−w; 05.70.Ce

##  I Introduction

An in-depth investigation into the impact of the gravitational field on the
dynamics of quantum mechanical systems remains a topic of great interest.
Albert Einstein’s general theory of relativity (GR) (key-1, ) offers an
engaging and all-encompassing portrayal of gravity as an intrinsic geometric
feature of spacetime. This theory sheds light on the profound link between the
curvature of spacetime and the emergence of the classical gravitational field,
resulting in highly successful predictions of remarkable phenomena such as
gravitational waves (key-2, ) and black holes (key-3, ). Concurrently, quantum
mechanics (QM) provides a robust framework for comprehending and describing
the intricate behavior of particles at the microscopic level (key-4, ). The
intersection of these two domains of physics holds promising potential for
unveiling deeper insights into the fundamental nature of the universe.

Quantum field theory has achieved remarkable success in deciphering the
complexities of interactions among subatomic particles and in shedding light
on the origins of the three fundamental forces in nature: the weak, strong,
and electromagnetic interactions (key-5, ). Nonetheless, the pursuit of a
unified theory capable of reconciling general relativity and quantum
mechanics, often referred to as a theory of quantum gravity, has long been
beset by persistent challenges and unresolved technical issues, at least until
very recently (key-6, ; key-7, ). These hurdles have spurred intense
scientific endeavors aimed at bridging the lingering gaps in our
understanding, as scientists work diligently to unveil the foundational
framework that harmonizes these two fundamental cornerstones of modern
physics.

Som and Raychaudhuri (key-07, ) introduced a set of stationary cylindrically
symmetric solutions to the Einstein–Maxwell equations, which describe a
charged dust distribution undergoing rigid rotation. In this solution, the
Lorentz force becomes zero everywhere, and the ratio of charge density to mass
density can take on any arbitrary value. Barrow and Dabrowski (key-08, )
demonstrated that in low-energy effective string theories, homogeneous Gödel-
type space-times may not contain closed time-like curves. They presented exact
solutions for the Gödel-type metric within string theory (key-09, ),
considering the full $O\left(\alpha\right)$ action, which includes both
dilaton and axion fields (key-08, ; key-09, ; key-010, ). It’s worth noting
that the Som-Raychaudhuri space-time belongs to the category of flat Gödel-
type solutions. Various aspects of Gödel-type solutions are elaborated upon in
(key-011, ; key-012, ; key-013, ; key-014, ). Gürses et al. illustrated
through several examples that Gödel-type metrics can be applied to derive
exact solutions in various supergravity theories, resulting in spacetimes that
may encompass closed time-like and closed null curves or none of these
features (key-015, ). Furthermore, Clifton et al. (key-016, ) identified the
general conditions for the existence of Gödel, Einstein static, and de-Sitter
universes in gravity theories that are derived from a Lagrangian defined as an
arbitrary function of the scalar curvature and Riemann curvature invariants.
They provided explicit expressions for these solutions in terms of the
Lagrangian parameters and determined the conditions under which time travel is
permissible in Gödel universes.

Numerous research studies have probed the examination of physical attributes
associated with various backgrounds in the context of Som Raychaudhuri
spacetime. These investigations encompass a wide array of phenomena,
including: (i) The characteristics of the rotating Som–Raychaudhuri
homogeneous spacetime. (ii) The relativistic quantum dynamics of spin-zero
particles in Som–Raychaudhuri spacetime under the gravitational influence of a
specific topology (key-017, ). (iii) The behavior of the Klein–Gordon
oscillator in Som–Raychaudhuri spacetime within a cosmic context (key-018, ).
(iv) The confinement of scalar particles in a linear fashion within
Som–Raychaudhuri spacetime (key-019, ), and (v) The confinement of scalar
particles in a topologically straightforward flat Gödel-type spacetime
(key-020, ).

Additionally, another reference, Ref. (key-021, ), explores the quantum
dynamics of scalar and spin-half particles in Gödel-type spacetimes
characterized by positive, negative, and zero curvatures. In Refs. (key-022, ;
key-023, ), the quantum dynamics of scalar particles in a particular category
of Gödel-type solutions are examined, revealing significant similarities in
energy levels to the Landau problem within flat, spherical, and hyperbolic
spaces. In Ref. (key-024, ), the investigation focuses on the quantum dynamics
of scalar particles within Som–Raychaudhuri spacetime, offering a comparison
with Landau levels in flat space. Ref. (key-025, ) delves into the quantum
dynamics of spin-half particles (Dirac fermions) within the backdrop of
Som–Raychaudhuri spacetime, featuring the presence of torsion and a cosmic
string traversing through it. The researchers observe a break in the
degeneracy of relativistic energy levels, and they find that the corresponding
eigenfunctions are influenced by the presence of the topological defect in the
background spacetime with torsion. Ref. (key-026, ) investigates the quantum
dynamics of spin-half particles (Weyl fermions) in Som–Raychaudhuri spacetime
featuring a topological defect, while in Ref. (key-027, ), the study explores
scalar quantum particles within a specific class of Gödel-type solutions with
a cosmic string intersecting the spacetime. Ref. (key-028, ) is dedicated to
the investigation of the Fermi field and Dirac oscillator within the context
of Som–Raychaudhuri spacetime.

In addition, Ref. (key-029, ) examines the Klein–Gordon equation when
subjected to vector and scalar potentials of Coulomb-type under the influence
of non-inertial effects in the cosmic string spacetime. Finally, Ref.
(key-030, ) investigates two distinct categories of solutions for the
Klein–Gordon equation in the presence of Coulomb-like scalar potentials while
considering non-inertial effects in the cosmic string spacetime.

This paper provides a comprehensive investigation into the dynamic behavior of
boson particles in the presence of a cosmic string in Som Raychaudhuri
spacetime. To do this we remark that: (i) we focuses on studying the effects
of a cosmic string on the free Klein-Gordon equation in Som Raychaudhuri
spacetime, analyzing how the equation is modified and its implications on the
Klein-Gordon field dynamics. (ii) Then, we extends its inquiry to the Klein-
Gordon oscillator in this spacetime context, providing an exact solution and
exploring the resulting energy spectrum. This comprehensive investigation
enhances our understanding of the Klein-Gordon equation’s behavior in the
presence of cosmic strings, offering insights into the quantized energy levels
and their implications for the universe’s dynamics, bridging theory and
observation in relativistic wave equations’ interactions with cosmic strings.

The outline of this paper is as follows: Section II is devoted as an overview
of the Klein-Gordon equation in curved spacetime. The solution of free and
Klein-Gordon oscillator are the main objects of both Sections III and IV.
Finally, we give conclusions in Section V.

##  II An Overview of the Klein-Gordon equation

In this section, our objective is to examine the Klein-Gordon oscillator (KGO)
within the framework of a cosmic string background geometry . It is widely
acknowledged that the relativistic wave equations for a scalar particle in a
Riemannian spacetime, defined by the metric tensor $g_{\alpha\beta}$ , can be
derived by reformulating the Klein-Gordon equation in a manner described in
textbooks such as (key-8, ; key-9, ; key-10, ; key-0101, ; key-0102, ;
key-0103, ).

$\left(\frac{1}{\sqrt{-g}}\partial_{\alpha}\left(\sqrt{-g}g^{\alpha\beta}\partial_{\beta}\right)-m^{2}-\xi
R\right)\bm{\phi}(\bm{r},t)=0,$ (1)

Here, we have the Laplace-Beltrami operator
$\square=\frac{1}{\sqrt{-g}}\partial_{\alpha}\left(\sqrt{-g}g^{\alpha\beta}\partial_{\beta}\right)$denoted
as $\nabla^{2}$ , $\xi$ represents a real dimensionless coupling constant, and
$R$ is the Ricci scalar curvature defined as
$R=g^{\alpha\beta}R_{\alpha\beta}$ , where $R_{\mu\nu}$ denotes the Ricci
curvature tensor. $g^{\alpha\beta}$ represents the inverse metric tensor, and
$g=\det(g_{\mu\nu})$.

Our objective is to investigate the quantum dynamics of spin-0 particles in
the spacetime induced by the Som-Raychaudhuri spacetime with cosmic string
oscillators.

##  III Free Klein-Gordon equation in Som–Raychaudhuri spacetime with a cosmic
string

Prior to delving into the Hamiltonian representation of the KGO, let us
commence by deriving the Klein-Gordon (KG) wave equation for a free
relativistic scalar particle in the context of a cosmic string spacetime. This
particular spacetime is presumed to be static and possess cylindrical
symmetry.

The line element that characterizes the cosmic string metric in a
(1+3)-dimensional Som-Raychaudhuri spacetime (with $\hbar=c=1$) is given by
(key-11, ; key-12, ; key-13, ; key-14, ):

$\displaystyle ds^{2}$ $\displaystyle=g_{\mu\nu}dx^{\mu}dx^{\nu}$
$\displaystyle=-\left(dt+\alpha\Omega
r^{2}d\varphi\right)^{2}+dr^{2}+\alpha^{2}r^{2}d\varphi^{2}+dz^{2},$ (2)

while the parameter $\alpha$ characterizes the cosmic string with
$\alpha\in\left[0,1\right]$ , The parameter $\Omega$ characterizes the
vorticity of the spacetime where

$ds^{2}=-dt^{2}-2\Omega\alpha
r^{2}dtd\varphi+dr^{2}+\left[\alpha^{2}r^{2}-\left(\alpha\varOmega
r^{2}\right)^{2}\right]d\varphi^{2}+dz^{2},$ (3)

Given the metric and inverse metric tensor components, represented as follows:

$g_{\mu\nu}=\left(\begin{array}[]{cccc}-1&0&-\alpha\Omega r^{2}&0\\\
0&1&0&0\\\ -\alpha\Omega r^{2}&0&\left[\alpha^{2}r^{2}-\left(\alpha\varOmega
r^{2}\right)^{2}\right]&0\\\ 0&0&0&1\end{array}\right),\quad
g^{\mu\nu}=\left(\begin{array}[]{cccc}\left(-1+\alpha\left(\Omega
r\right)^{2}\right)&0&-\Omega&0\\\ 0&1&0&0\\\ -\Omega&0&\frac{1}{\left(\alpha
r\right)^{2}}&0\\\ 0&0&0&1\end{array}\right)$ (4)

After performing some straightforward algebraic manipulations, we obtain the
following second-order differential equation for the radial function
$\psi(r)$:

$\left[\left(-1+\alpha\left(\Omega
r\right)^{2}\right)\frac{\partial^{2}}{\partial
t^{2}}+\frac{1}{\sqrt{-g}}\frac{\partial}{\partial
r}\left(\sqrt{-g}\frac{\partial}{\partial
r}\right)-\frac{1}{\alpha^{2}r^{2}}\frac{\partial^{2}}{\partial\varphi^{2}}+\frac{\partial^{2}}{\partial
z^{2}}-2\varOmega\left(\frac{\partial}{\partial
t}\frac{\partial}{\partial\varphi}\right)-m^{2}\right]\bm{\phi}\left(\bm{r}\right)=0$
(5)

The wave function of this system is defined by

$\bm{\phi}\left(\bm{r}\right)=e^{-iEt+i\ell\varphi+iKz}\psi\left(r\right)$ (6)

Where $\ell=0,\pm 1,\pm 2,\pm 3....$. By substituting the last equation into
the second-order differential equation, we obtain:

$\left[\frac{d^{2}}{dr^{2}}+\frac{1}{r}\frac{d}{dr}-\frac{\left(\ell\right)^{2}}{\alpha^{2}r^{2}}-\alpha\left(\Omega
E\right)^{2}r^{2}+E^{2}-m^{2}-K^{2}-2\ell\varOmega
E\right]\psi\left(r\right)=0$ (7)

setting $\gamma=E^{2}-m^{2}-K^{2}-2\ell\varOmega E,$ yields

$\left[\frac{d^{2}}{dr^{2}}+\frac{1}{r}\frac{d}{dr}-\frac{\ell^{2}}{\alpha^{2}r^{2}}-\alpha\left(\Omega
E\right)^{2}r^{2}+\gamma\right]\psi\left(r\right)=0,$ (8)

Observing Eq. (8) we can note that, although the particle is considered
"free", in fact, in the radial direction it is subject to a harmonic-type
central potential $(-\alpha\left(\Omega E\right)^{2}r^{2})$. It is worth
mentioning that this potential has a gravitational nature, that is, it was
induced by the background characterized by the metric given in Eq. (3). The
exact solution of this The exact solutions to this differential equation are
given by Whittaker functions key-14a , where:

$\displaystyle\psi\left(r\right)$
$\displaystyle=\mathcal{C}_{1}r^{-1}\mathrm{WhittakerM}\left(\frac{\gamma}{4\left(\Omega
E\alpha^{1/2}\right)},\frac{\ell}{2\alpha},\alpha^{1/2}\Omega E\,r^{2}\right)$
$\displaystyle+\mathcal{C}_{2}r^{-1}\mathrm{WhittakerW}\left(\frac{\gamma}{4\left(\Omega
E\alpha^{1/2}\right)},\frac{\ell}{2\alpha},\alpha^{1/2}\Omega E\,r^{2}\right)$
(9)

by using this condition of the wave function $\psi\left(0\right)=0,$ and
$\underset{r\rightarrow+\infty}{Lim}\psi\left(r\right)=0$, suggest the exact
wave function of the system,where

$\psi\left(r\right)=\mathcal{N}_{1}r^{-1}\mathrm{WhittakerM}\left(\frac{\gamma}{4\left(\Omega
E\alpha^{1/2}\right)},\frac{\ell}{2\alpha},\alpha^{1/2}\Omega E\,r^{2}\right)$
(10)

where $\mathcal{N}_{1}$ represents the normalization condition, The
relationship between Whittaker functions $WhittakerM\left(a,b,z\right)$ and
hypergeometric polynomials ${}_{1}F_{1}\left(a,b,z\right)$ is given by key-14b
:

$WhittakerM\left(a,b,z\right)=z^{b+\frac{1}{2}}e^{-z/2}{}_{1}F_{1}\left(\frac{1}{2}-a+b,2b+1,z\right)$
(11)

The final relation of the wave function with the hypergeometric polynomial is
given as:

$\psi\left(r\right)=\mathcal{N}_{1}r^{-1}\mathrm{e}^{\frac{\Omega
E\alpha^{\frac{1}{2}}\,r^{2}}{2}}\left(\alpha^{\frac{1}{2}}\Omega
E\,r^{2}\right){}^{\frac{\alpha+\ell}{2\alpha}}\mathrm{{}_{1}F_{1}}\left(-\frac{-2E\Omega\,\alpha^{\frac{3}{2}}-2E\Omega\ell\alpha^{\frac{1}{2}}+\alpha\left(-2\ell
E\Omega+E^{2}-K^{2}-m^{2}\right)}{4\alpha^{\frac{3}{2}}E\Omega},1+\frac{\ell}{\alpha},\alpha^{\frac{1}{2}}\Omega
E\,r^{2}\right)$ (12)

We should note that in equation (12), the solution must be a polynomial
function of degree $n$. However, when $n\to\infty$, a divergence issue arises.
We can only have a finite polynomial if the factor of the first term in
equation (12) is a negative integer, indicating that:

$\frac{2E\Omega\,\alpha^{\frac{3}{2}}+2E\Omega\ell\alpha^{\frac{1}{2}}+\alpha\left(2\ell
E\Omega-E^{2}+K^{2}+m^{2}\right)}{4\alpha^{\frac{3}{2}}E\Omega}=-n$ (13)

By utilizing this result and substituting the parameters from equation (13),
we can determine the quantized energy spectrum of the free Klein-Gordon
equation within the Som-Raychaudhuri spacetime of the cosmic string.
Therefore, we obtain:

$\displaystyle E_{n}^{\pm}$
$\displaystyle=\pm\Omega\left[\left(2n+1\right)\,\alpha^{\frac{1}{2}}+\ell\left(1+\alpha^{-\frac{1}{2}}\right)\right]$
(14)
$\displaystyle\pm\sqrt{\frac{\left(4\Omega^{2}\ell\left(n+\frac{1}{2}\right)\alpha^{\frac{3}{2}}+2\alpha^{\frac{1}{2}}\,\Omega^{2}\ell^{2}+\left(4\left(n+\frac{1}{2}\right)^{2}\alpha^{2}+\left(\ell^{2}+\left(4n+2\right)\ell\right)\alpha+\ell^{2}\right)\Omega^{2}+\alpha\left[m^{2}+K^{2}\right]\right)}{\alpha}}$
(15)

Equation (15) displays the energy spectrum of the free Klein-Gordon equation
in the context of the Som-Raychaudhuri spacetime. The form of this equation is
dependent on different geometrical parameters of the spacetime. To understand
the effect of these parameters on the energy levels, figures. 1 and 2 have
been constructed for this purpose. Based on the two figures, we can observed
the following :

(a) here $\ell=1$ (b) here $\ell=0$

Figure 1: Spectrum of energy versus quantum number $n$ for different values of
$\varOmega$ and $\ell=0,1$. here $m=\omega=1,\alpha=0.5,K=0$

(a) here $\ell=1$ (b) here $\ell=0$

Figure 2: Spectrum of energy versus $\varOmega$ for four level $n=0,1,2,3$ and
$\ell=0,1$. here $m=\omega=1,\alpha=0.5,K=0$

(a) here $\ell=1$ (b) here $\ell=0$

Figure 3: Spectrum of energy versus $\alpha$ for four level $n=0,1,2,3$ and
$\ell=0,1$. here $m=\omega=1,\alpha=0.5,K=0$

In Figure 1, we illustrate the energy levels of the free Klein-Gordon equation
when operating within the framework of Some-Raychaudhuri spacetime in function
of the quantum number $n$ . In this investigation, we have standardized
certain key parameters: both mass ($m$) and frequency ($w$) are set to a value
of 1, while the parameters $\alpha=0.5$ and $K=0$. We have systematically
explored various scenarios, altering the value of the parameter $\Omega$. Two
specific cases have been carefully examined: in figure(1.a), the angular
momentum $\ell=1$ , while in figure(1.b), $\ell=0$. Our primary goal has been
to gain a deep understanding of how the $\Omega$ term influences the structure
of the spacetime geometry and to discern its effectiveness in shaping the
dynamic behavior of energy within the system. These findings have significant
implications for advancing our comprehension of how the motion of particles
behave in the context of curved spacetime.

Figure 2 present the energy spectrum of the free Klein-Gordon equation within
the framework of Some-Raychaudhuri spacetime for different values of
$\varOmega$ using the same adjustable parameters. This study encompasses a
thorough exploration of various quantum number values $n=0,1,2,3$) within
different visions. Specifically, we investigate two cases: case where the
orbital angular momentum quantum number ($\ell$) is set to 1, and the other
with $\ell=0$. Our inquiry extends across the spectrum of geometrical
parameter values within the interval [0, 1], focusing on the impact of the
$\Omega$ term in relation to the spacetime geometry. Our findings illuminate
that the influence of the $\Omega$ term on the geometric spacetime structure
is consistently effective across all quantum number levels, thus underscoring
its significance in shaping the energy spectrum of the Klein-Gordon equation
in Some-Raychaudhuri spacetime.

Finally, Figure 3 depict the Spectrum of energy versus $\alpha$ for four level
$n=0,1,2,3$ and $\ell=0,1$ within the context of Some-Raychaudhuri spacetime.
two distinct scenarios can be study: case ’a,’ where the angular momentum
($\ell=1$) and the other where $\ell=0$. While we explore different quantum
number levels ($n=0,1,2,3$), a conspicuous influence of the $\alpha$ term
emerges consistently across all these levels. In the instance of $\ell=1$ and
$\alpha=0$, a striking observation surfaces, where the energy levels approach
both positive and negative infinity, indicating the presence of a pole in the
energy spectrum. This phenomenon signifies the crucial role that the
topological defect plays in modifying energy levels when $\ell=1$. In
contrast, for $\ell=0$, we observe a symmetrical energy spectrum, with the
impact of the topological defect maintaining a high degree of effectiveness,
continuously influencing energy levels. These remarks shed light on the
profound impact of topological defects on the dynamic behavior of energy
within the Klein-Gordon equation, highlighting their intricate interaction
with spacetime geometry and quantum properties.

In conclusion, the analysis of the energy spectrum of the free Klein-Gordon
equation within Some-Raychaudhuri spacetime leads to a significant revelation:
the quantization of energy levels, expressed as $E^{\pm}=f(n)$. This
quantization emphasizes the pivotal role played by the geometrical parameter
defined in the initial term of the inverse metric component $g^{00}$. The
significance of this observation lies in its direct correlation to the
underlying spacetime geometry. The inverse metric component $g^{00}$ captures
the gravitational field’s influence on the energy of Klein-Gordon particles,
rendering it an indispensable factor in our comprehension of how gravitation
affects the quantum behavior of particles within this specific spacetime. As a
consequance, this finding signifies a profound connection between spacetime
geometry and the quantized energy levels of particles, unveiling an intriguing
link between general relativity and quantum mechanics within the framework of
the Klein-Gordon equation in Some-Raychaudhuri spacetime. In addition, These
observations illuminate the intricate relationship between particle dynamics
and the underlying spacetime geometry. The parameter $\Omega$ plays a pivotal
role in shaping this interaction, emphasizing the profound interplay between
the fundamental constituents of the universe and the fabric of this spacetime.
in the case of $\left(\Omega=0\right)$, the spectrum of the free Klein-Gordon
equation within the Som-Raychaudhuri spacetime of the cosmic string is given
by $E^{\pm}=\pm\sqrt{m^{2}+K^{2}}$.

In the next section of this investigation, we will introduce the the
interaction of the Dirac oscillator.

##  IV Klein-Gordon oscillator in Som–Raychaudhuri spacetime with a cosmic
string

In this section, our interest is to describe the quantum dynamics of a
relativistic oscillator model in spacetime described by the metric given in
Eq. (3). This oscillator model is known in the literature as the Klein-Gordon
oscillator (KGO) kgo , which has become an object of study in several branches
of physics due to its unique characteristics that other models of relativistic
oscillators do not have. Among these characteristics is analyticity, that is,
it is possible to describe it completely analytically, without needing
numerical or approximate methods to obtain its particular solution or chaos.
Another feature that makes it very interesting is the recovery of the
Schrondiger oscillator in the non-relativistic regime kgo1 .

KGO has been investigated in several relativistic quantum mechanics scenarios,
for example, subjected to the central potentials in Minkowski spacetime kgo2 ;
kgo3 ; kgo4 , in cosmic string spacetime kgo5 , in global monopole spacetime
kgo6 , in Kaluza-Klein theory kgo7 ; kgo8 ; kgo9 , and in possible scenarios
of Lorentz symmetry violation kgo10 ; kgo11 .

We begin by considering a scalar quantum particle residing in the
gravitational field of the spacetime described by the metric (2). To
incorporate this, we introduce a modification of the momentum operator,
replacing $p_{i}$ with $p_{i}\longrightarrow p_{i}+im\omega x_{i}$ , where
$p_{i}=i\nabla_{i}$ in Eq (8).

By following the same steps as before, we derive the following radial
equation:

$\left[\frac{d^{2}}{dr^{2}}+\frac{1}{r}\frac{d}{dr}-\frac{\ell^{2}}{\alpha^{2}r^{2}}-\left[m^{2}\omega^{2}+\alpha\left(\Omega
E\right)^{2}\right]r^{2}+\delta\right]\psi\left(r\right)=0,$ (16)

By observing Eq. (16) we can note that that the oscillator term remains,
however, this term is effected by the term arising from the non-minimal
coupling in the Klein-Gordon equation, which guarantees the presence of the
KGO.

Here, we have defined:

$\delta=E^{2}-m^{2}-K^{2}-2\ell\varOmega E+2m\omega.$ (17)

Following mathematical computations, it becomes possible to present the
precise expression of the wave function for the analyzed system.

$\displaystyle\psi\left(r\right)$
$\displaystyle=\mathcal{C}_{1}r^{-1}\mathrm{WhittakerM}\left(\frac{\delta}{4\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}},\frac{\ell}{2\alpha},\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,r^{2}\right)$
$\displaystyle+\mathcal{C}_{2}r^{-1}\mathrm{WhittakerW}\left(\frac{\delta}{4\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}},\frac{\ell}{2\alpha},\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,r^{2}\right)$ (18)

By applying convergence criteria to the previously utilized wave functions, it
is possible to evaluate the following equation as a potential wave function.

$\psi\left(r\right)=\mathcal{N}_{2}\mathrm{WhittakerM}\left(\frac{\delta}{4\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}},\frac{\ell}{2\alpha},\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,r^{2}\right)$ (19)

The primary goal of mathematical approximations is to consistently discover
actual solutions that elucidate concealed physical phenomena. In the realm of
scientific inquiry, the ability to accurately model and understand the
behavior of complex systems is of paramount importance. By employing
mathematical conversions, such as transitioning from Whittaker functions to
hypergeometric functions, researchers can navigate the intricate landscape of
quantum mechanics, particle physics, and other branches of scientific study.
These conversions serve as powerful tools that allow for a deeper exploration
of the underlying principles governing the universe. They provide a means to
bridge the gap between abstract mathematical formulations and tangible
observations, facilitating the interpretation and prediction of experimental
results. As these conversions unfold, revealing the intricate relationship
between various mathematical constructs, researchers gain valuable insights
into the fundamental nature of the systems under investigation. Through this
process, new connections and patterns emerge, shedding light on previously
uncharted aspects of the physical world and paving the way for further
scientific advancements. Thus, the application of mathematical conversions,
particularly the transition from Whittaker to hypergeometric functions, serves
as a gateway to unraveling the mysteries that lie hidden within the fabric of
our reality.

$\displaystyle\psi\left(r\right)$
$\displaystyle=\mathcal{N}_{2}r^{-1}\mathrm{e}^{-\frac{\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,r^{2}}{2}}\left(\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,r^{2}\right){}^{\frac{\alpha+\ell}{2\alpha}}$
$\displaystyle\mathrm{{}_{1}F_{1}}\left(-\frac{(-2\ell-2\alpha)\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}+(-2\ell\Omega
E+E^{2}-K^{2}-m^{2}+2m\omega)\alpha}{4\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,\alpha},1+\frac{\ell}{\alpha},\sqrt{\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}}\,r^{2}\right)$ (20)

In the quest for a comprehensive understanding of the studied system, the
culmination of mathematical approximations leads us to the solution of the
final equation for the wave functions. This solution is expressed in terms of
hypergeometric functions, which play a vital role in capturing the intricate
behavior of quantum systems. The hypergeometric function, with its powerful
mathematical properties, enables us to unravel the complexities of the system
and explore its underlying dynamics in greater detail. By providing a precise
and elegant mathematical representation, this solution unveils the intricate
relationships between the various elements of the system, shedding light on
the hidden physical phenomena at play. Through this remarkable feat of
mathematical analysis, we are able to grasp a deeper understanding of the
system’s behavior and uncover profound insights into the nature of the
spectrum of energy. Again, The asymptotic behavior of the confluent
hypergeometric function implies that

$\frac{E^{2}-m^{2}-K^{2}-2\ell\varOmega E+2m\omega}{4\sqrt{\left(\alpha
E^{2}\Omega^{2}+m^{2}\omega^{2}\right)}}=-n,$ (21)

Indeed, it is acknowledged that the equation at hand lacks an exact and
explicit solution due to its inherent complexity and difficulty. Such
intricate equations often pose significant challenges when seeking closed-form
solutions. However, to facilitate a deeper understanding and simplify the
analysis, we can focus on obtaining the exact form of the system’s energy.
Remarkably, the energy expression is derived and presented in the form of a
fourth-degree equation. While the complexity remains, this formulation
provides a valuable stepping stone for further investigation and analysis. By
examining the energy equation, we can discern critical characteristics and
properties of the system’s energy landscape, allowing us to gain insights into
the system’s behavior, stability, and possible energy states. While the
equation may present mathematical and computational challenges, its exact form
grants us an invaluable starting point for further exploration and deeper
comprehension of the underlying physical phenomena.

After streamlining the mathematical calculations, we successfully unveil the
energy spectrum of the system, representing a significant milestone in our
analysis. Through meticulous simplifications and computations, we arrive at an
explicit form that characterizes the system energy states. The energy spectrum
emerges in a distinct and compelling fashion, offering valuable insights into
the system’s behavior and the quantized nature of its energy levels where

$\alpha^{2}E^{4}-4\ell\Omega\alpha^{2}E^{3}-aE^{2}+bE-c=0$ (22)

with

$\displaystyle a$
$\displaystyle=16\Omega^{2}\alpha^{3}n^{2}+16\Omega^{2}\alpha^{3}n-4\Omega^{2}\alpha^{2}\ell^{2}+16\Omega^{2}\alpha^{2}\ell
n+4\Omega^{2}\alpha^{3}+8\Omega^{2}\alpha^{2}\ell+4\Omega^{2}\alpha\,\ell^{2}+2K^{2}\alpha^{2}+2\alpha^{2}m^{2}-4\alpha^{2}m\omega$
$\displaystyle b$
$\displaystyle=4\ell\Omega\alpha^{2}\left[m^{2}+K^{2}\right]-8\Omega\,\alpha^{2}\ell
m\omega$ $\displaystyle c$
$\displaystyle=16\alpha^{2}m^{2}n^{2}\omega^{2}+16\alpha^{2}m^{2}n\omega^{2}+16\alpha\ell
m^{2}n\omega^{2}-K^{4}\alpha^{2}-2K^{2}\alpha^{2}m^{2}+4K^{2}\alpha^{2}m\omega-\alpha^{2}m^{4}+4\alpha^{2}m^{3}\omega+8\alpha\ell
m^{2}\omega^{2}+4\ell^{2}m^{2}\omega^{2}$

The energy spectrum $E^{\pm}\left(n\right)$ (Eq. (22)is an algebraic equation
of the degree 4 having both real and complex solutions. The complex solutions
are not physical, but there are two other real solutions. The energy spectrum
will be discussed for different values of $\varOmega$ and $\ell$. To better
understand the behavior of our energy spectrum, we can consider two
situations. The first one is the case when $\varOmega=0$, and the second is
when $\varOmega\neq 0$.

For the first case when $\varOmega=0$, it represents a special case that
allows us to derive the energy spectrum associated with the extensively
researched findings by Boumali and Messai (kgo5, ). In their comprehensive
investigation, they delved into how the topological defect constant, denoted
as $\alpha$, influences the energy spectrum of cosmic strings. The topological
defect constant $\alpha$ is a pivotal factor in determining the resulting
energy spectrum, with its definition stemming from the physical attributes and
geometric configuration of cosmic strings. The outcomes of their research
underscore the substantial impact of $\alpha$ values on the energy
distribution. Specifically, when $\omega$ is set to zero, the resulting
findings align with the extensively explored spectrum outlined in reference
(kgo5, ).

In addition, their study contributes significantly to advancing our
comprehension of the intricate interplay between topological defect constants
and the energy spectrum of cosmic strings. By delving into the characteristics
and properties of these topological defects, researchers can uncover the
fundamental mechanisms governing the formation, evolution, and behavior of
cosmic strings. The energy spectrum derived in the special scenario where
$\Omega=0$ holds particular importance as it provides insights into the
specific dynamics and quantum nature of cosmic strings when other contributing
factors are absent. where:

$E^{\pm}\left(n\right)=\pm\sqrt{\left(4nm\omega+\frac{2m\omega\left|\ell\right|}{\alpha}+m^{2}+K^{2}\right)}$
(23)

Now, let’s examine the scenario where $\varOmega$ is not equal to 0, and in
this context, we can distinguish between two cases.

  * •

The first Scenario (When $\ell=0$): In this case, the numerical values of the
spectrum of energy are given into Table. 1. This table provides a
comprehensive summary of the energy levels within the system under
investigation, encompassing quantum numbers within the range of $[0,21]$, with
a fixed value of the parameter $\alpha$ set to $0.5$. The obtained results
enable a comprehensive exploration of the system’s quantum characteristics.
The associated values have been plotted for various $\varOmega$ values in
Figure. 4. As shown in this figure, the energy spectrum displays symmetry and
increases with growing $\varOmega$.

  * •

The second Scenario (With $\ell=1$): In this scenario, specific numerical
values of the energy spectrum, as discussed in the previous section, are
reported in Table 2. These values have been visualized in Figure. 5 for
various $\varOmega$ values, while maintaining a fixed value of the parameter
$\alpha$ at $0.5$. Contrarily the previous case, the energy spectrum in this
scenario exhibits asymmetry.

In summary, this research paper’s thorough investigation significantly
enhances our comprehension of how the Klein-Gordon equation behaves within the
context of Som Raychaudhuri spacetime when influenced by a cosmic string. The
findings obtained through this study contribute to a deeper understanding of
relativistic wave equations and their interactions with cosmic structures.
Moreover, the insights garnered from this research have broad-reaching
implications for advancing our understanding of the universe’s dynamics,
encompassing both theoretical progress and potential links to observable
phenomena.

Moving forward, we plan to replicate this study with varying components and
explore different mathematical approximations. Additionally, we intend to
investigate the thermal characteristics of the materials involved and employ
the concept of generalization to develop more precise approximation models,
drawing upon the Feshbach-Villars approach.

##  V Conclusion

"This paper offers a comprehensive examination of the behavior of the Klein-
Gordon equation within the context of Som Raychaudhuri spacetime when
influenced by a cosmic string. We establish the fundamental significance of
the Klein-Gordon equation in theoretical physics, emphasizing its role as a
foundational framework for describing relativistic wave equations. This
foundational understanding forms the basis for our exploration of the
equation’s behavior when cosmic strings are introduced.

Subsequently, we delve into the modified behavior of the free Klein-Gordon
equation when a cosmic string is present in Som Raychaudhuri spacetime. This
analysis takes into account the effects of the cosmic string, revealing
insights into the alterations in the equation’s dynamics and their
implications for the behavior of the Klein-Gordon field.

In the final phase of our study, we extend our investigation to the Klein-
Gordon oscillator within Som Raychaudhuri spacetime with a cosmic string.
Through the examination of an exact solution, our research delves into the
energy spectrum associated with this system. These inquiries provide valuable
insights into the quantization of energy levels, shedding light on the
dynamics of the Klein-Gordon oscillator."

## References

  * (1) A. Einstein, Annalen Phys. 49, 769 (1916).
  * (2) B. P. Abbott et al, Phys Rev Lett 116, 061102 (2016).
  * (3) K. Akiyama et al, Astrophys J Lett 875, L1 (2019).
  * (4) R. P. Feynman, and A. R. Hibbs, Quantum mechanics and path integrals, Courier Corporation(1965).
  * (5) M. D. Schwartz, Quantum field theory and the standard model, Cambridge University Press (2013).
  * (6) A. Ashtekar, and J. J. Stachel, Conceptual problems of quantum gravity, Birkhäuser (1991).
  * (7) L. Smolin, The trouble with physics: The rise of string theory, the fall of a science, and what comes next, Mariner Books (2007).
  * (8) M.M. Som, A.K. Raychaudhuri, Proc. R. Soc. A 304, 81 (1968).
  * (9) J.D. Barrow, M.P. Dabrowski, Phys. Rev. D 58, 103502 (1998).
  * (10) O. Bertolami, F. Lobo, Neuro Quantol. 7, 1 (2009).
  * (11) P. Kanti, C.E. Vayonakis, Phys. Rev. D 60, 103519 (1999).
  * (12) J.D. Barrow, C. Tsagas, Class. Quantum Grav. 21, 1773 (2004)
  * (13) J.D. Barrow, C. Tsagas, Phys. Rev. D 69, 064007 (2004).
  * (14) F.M. Paiva, M.J. Reboucas, A.F.F. Teixeira, Phys. Lett. A 126, 168 (1987).
  * (15) R.J. Gleiser, M. Gürses, A. Karasu, S. Ozgur, Class. Quantum Grav. 23, 2653 (2006).
  * (16) M. Gürses, A. Karasu, Ö. Sarioğlu, Class. Quantum Grav. 22, 1527 (2018).
  * (17) T. Clifton, J. Barrow, Phys. Rev. D 72, 123003 (2005).
  * (18) Z. Wang, Z. Long, C. Long, M. Wu, EPJ Plus 130, 36 (2015).
  * (19) J. Carvalho, A.M. de M. Carvalho, C. Furtado, EPJ C 74, 2935 (2014).
  * (20) R.L.L. Vitoria, C. Furtado, K. Bakke, EPJ C 78, 44 (2018).
  * (21) F. Ahmed, EPJ C 79(02), 104 (2019).
  * (22) B.D.B. Figueiredo, I.D. Soares, J. Tiomno, Class. Quantum Grav. 9, 1593 (1992).
  * (23) N. Drukker, B. Fiol, J. Simon, JCAP 410, 012 (2004).
  * (24) N. Drukker, B. Fiol, J. Simon, Phys. Rev. Lett. 91, 231601 (2003).
  * (25) S. Das, J. Gegenberg, Gen. Relativ. Gravit. 40, 2115 (2008).
  * (26) G.Q. Garcia, J.R. de S. Oliveira, K. Bakke, C. Furtado, EPJ Plus 132, 123 (2017).
  * (27) G.Q. Garcia, J.R. de S. Oliveira, C. Furtado, Int. J. Mod. Phys. 27, 1850027 (2018).
  * (28) J. Carvalho, A.M. de M. Carvalho, E. Cavalcante, C. Furtado, EPJ C 76, 365 (2016).
  * (29) M. de Montigny, S. Zare, H. Hassanabadi, Gen. Relativ. Gravit. 50, 47 (2018).
  * (30) L.C.N. Santos, C.C. Barros Jr., EPJC 78, 13 (2018).
  * (31) L.C.N. Santos, C.C. Barros Jr., EPJ C 77, 186 (2017).
  * (32) N. D. Birrell and P. Davies, Quantum fields in curved space, Cambridge University Press (1984).
  * (33) L. Parker and D. J. Toms, Quantum field theory in curved spacetime: Quantized fields and gravity, Cambridge University Press. (2009).
  * (34) A. Bouzenada, A. Boumali, Ann. Physics 452, 169302 (2023).
  * (35) A. Bouzenada, A. Boumali, R.L.L. Vitoria, F. Ahmed and M. Al-Raeei, Nuclear Physics B, 994, 116288 (2023).
  * (36) A. Bouzenada, A. Boumali and F. Serdouk, Theoret. and Math. Phys,216, 1055–1067 (2023).
  * (37) A. Bouzenada, A. Boumali, and E. O. Silva, Ann. Physics, 458,169479 (2023).
  * (38) P. Sedaghatnia, H. Hassanabadi, and F. Ahmed. Eur. Phys. J. C 79,1-8(2019).
  * (39) H. Hassanabadi, S. Zare, and M. D. Montigny. Gen. Relativ. Gravit. 50(8),104 (2018).
  * (40) R. L. L.Vitoria, C. Furtado, and K. Bakke. Eur. Phys. J. C 78(1),1-5 (2018).
  * (41) O. Mustafa. Eur. Phys. J. Plus 138(1) ,1-11 (2023)
  * (42) G. B. Arfken, H. J. Weber, Mathematical Methods for Physicists, 6th edn. (Elsevier Academic Press, New York, 2005).
  * (43) R L L Vitoria, H Belich, Phys. Scr. 94, 125301 (2019).
  * (44) S. Bruce, P. Minning, Nuovo Cimento A 106, 711 (1993).
  * (45) N. A. Rao, B. A. Kagali, Phys. Scr. 77, 015003 (2008).
  * (46) K. Bakke, C. Furtado, Ann. Phys. 355, 48 (2015).
  * (47) R. L. L. Vitoria, K. Bakke, Eur. Phys. J. Plus 131, 36 (2016).
  * (48) R. L. L. Vitoria, C. Furtado, K. Bakke, Ann. Phys. 370, 128 (2016).
  * (49) A. Boumali, N. Messai, Can. J. Phys. 92, 1460 (2014)
  * (50) E. A. F. Bragança, R. L. L. Vitória, H. Belich, E. R. Bezerra de Mello, Eur. Phys. J. C 80, 206 (2020).
  * (51) Josevi Carvalho, Alexandre M. de M. Carvalho, Everton Cavalcante, Claudio Furtado, Eur. Phys. J. C 76, 365 (2016).
  * (52) E. V. B. Leite, H. Belich, R. L. L. Vitória, Braz. J. Phys. 50, 744 (2020).
  * (53) E. V. B. Leite, H. Belich, R. L. L. Vitória, Mod. Phys. Lett. A 35, 2050283 (2020).
  * (54) R. L. L. Vitória, H. Belich, K. Bakke, Eur. Phys. J. Plus 132, 25 (2017).
  * (55) R. L. L. Vitória, H. Belich, Eur. Phys. J. C 78, 999 (2018). .
  * (56) A. Boumali and N. Messai, Can. J. Phys. 92, 1460 (2014).

Table 1: Some values of energies for $\ell=0,m=\omega=1,\alpha=0.5,K=0$ Quantum number, $n$ | $\Omega=0.25$ | $\Omega=0.5$ | $\Omega=0.75$ | $\Omega=1$
---|---|---|---|---
| $E^{+}$ | $E^{-}$ | $E^{+}$ | $E^{-}$ | $E^{+}$ | $E^{-}$ | $E^{+}$ | $E^{-}$
0 | 01.01587 | -01.01587 | 1.06651 | -01.06651 | 01.16144 | -01.16144 | 01.31607 | -01.31607
1 | 01.98577 | -01.98577 | 2.40511 | -02.40511 | 03.16559 | -03.16559 | 04.13647 | -04.13647
2 | 02.96094 | -02.96094 | 3.86966 | -03.86966 | 05.33645 | -05.33645 | 07.02548 | -07.02548
3 | 03.78960 | -03.78960 | 5.27159 | -05.27159 | 07.46734 | -07.46734 | 09.87459 | -09.87459
4 | 04.54542 | -04.54542 | 6.65891 | -06.65891 | 09.58863 | -09.58863 | 12.71230 | -12.71230
5 | 05.26144 | -05.26144 | 8.04526 | -08.04526 | 11.70748 | -11.70748 | 15.54566 | -15.54566
6 | 05.95444 | -05.95444 | 9.43425 | -09.43425 | 13.82584 | -13.82584 | 18.37700 | -18.37700
7 | 06.63386 | -06.63386 | 10.82655 | -10.82655 | 15.94430 | -15.94430 | 21.20730 | -21.20730
8 | 07.30538 | -07.30538 | 12.22191 | -12.22191 | 18.06301 | -18.06301 | 24.03700 | -24.03700
9 | 07.97257 | -07.97257 | 13.61993 | -13.61993 | 20.18202 | -20.18202 | 26.86632 | -26.86632
10 | 08.63771 | -08.63771 | 15.02016 | -15.02016 | 22.30130 | -22.30130 | 29.69541 | -29.69541
11 | 09.30230 | -09.30230 | 16.42223 | -16.42223 | 24.42081 | -24.42081 | 32.52434 | -32.52434
12 | 09.96728 | -09.96728 | 17.82582 | -17.82582 | 26.54053 | -26.54053 | 35.35315 | -35.35315
13 | 10.63327 | -10.63327 | 19.23069 | -19.23069 | 28.66043 | -28.66043 | 38.18189 | -38.18189
14 | 11.30066 | -11.30066 | 20.63663 | -20.63663 | 30.78048 | -30.78048 | 41.01056 | -41.01056
15 | 11.96966 | -11.96966 | 22.04347 | -22.04347 | 32.90066 | -32.90066 | 43.83919 | -43.83919
16 | 12.64037 | -12.64037 | 23.45108 | -23.45108 | 35.02095 | -35.02095 | 46.66778 | -46.66778
17 | 13.31285 | -13.31285 | 24.85934 | -24.85934 | 37.14134 | -37.14134 | 49.49634 | -49.49634
18 | 13.98707 | -13.98707 | 26.26817 | -26.26817 | 39.26181 | -39.26181 | 52.32489 | -52.32489
19 | 14.66300 | -14.66300 | 27.67749 | -27.67749 | 41.38235 | -41.38235 | 55.15342 | -55.15342
20 | 15.34057 | -15.34057 | 29.08724 | -29.08724 | 43.50296 | -43.50296 | 57.98193 | -57.98193
21 | 16.01971 | -16.01971 | 30.49737 | -30.49737 | 45.62363 | -45.62363 | 60.81043 | -60.81043
Figure 4: Plots of the energy of KG oscillator for different values of $\Omega$ with the parameters $K=0$ and $j=m=\omega=1,\varOmega\neq 0\,\ell=0.$ Table 2: Some values of energies with $\ell=1,m=\omega=1,\alpha=0.5,K=0$ Quantum number, $n$ | $\Omega=0.25$ | $\Omega=0.5$ | $\Omega=0.75$ | $\Omega=1$
---|---|---|---|---
| $E^{+}$ | $E^{-}$ | $E^{+}$ | $E^{-}$ | $E^{+}$ | $E^{-}$ | $E^{+}$ | $E^{-}$
0 | 02.48636 | -02.17462 | 03.45262 | -02.09056 | 05.78575 | -02.00759 | 09.36895 | -01.93775
1 | 03.25945 | -02.94186 | 04.80860 | -03.22572 | 07.78989 | -03.61904 | 11.80604 | -04.01022
2 | 04.02474 | -03.69798 | 06.20194 | -04.48998 | 09.86040 | -05.54130 | 14.44309 | -06.54486
3 | 04.75609 | -04.41863 | 07.59753 | -05.80549 | 11.95122 | -07.56557 | 17.15929 | -09.22120
4 | 05.46202 | -05.11344 | 08.99388 | -07.14966 | 14.05140 | -09.63039 | 19.91406 | -11.95608
5 | 06.15127 | -05.79174 | 10.39161 | -08.51195 | 16.15692 | -11.71484 | 22.69042 | -14.72094
6 | 06.83007 | -06.46003 | 11.79098 | -09.88638 | 18.26588 | -13.81021 | 25.48007 | -17.50331
7 | 07.50259 | -07.12265 | 13.19200 | -11.26928 | 20.37723 | -15.91227 | 28.27850 | -20.29680
8 | 08.17165 | -07.78247 | 14.59451 | -12.65828 | 22.49032 | -18.01872 | 31.08301 | -23.09781
9 | 08.83909 | -08.44136 | 15.99835 | -14.05181 | 24.60472 | -20.12821 | 33.89193 | -25.90415
10 | 09.50617 | -09.10056 | 17.40334 | -15.44876 | 26.72014 | -22.23989 | 36.70413 | -28.71439
11 | 10.17367 | -09.76085 | 18.80933 | -16.84838 | 28.83637 | -24.35321 | 39.51884 | -31.52759
12 | 10.84216 | -10.42274 | 20.21618 | -18.25009 | 30.95324 | -26.46778 | 42.33554 | -34.34308
13 | 11.51193 | -11.08650 | 21.62377 | -19.65348 | 33.07065 | -28.58332 | 45.15380 | -37.16038
14 | 12.18320 | -11.75228 | 23.03200 | -21.05824 | 35.18851 | -30.69965 | 47.97335 | -39.97913
15 | 12.85605 | -12.42015 | 24.44078 | -22.46412 | 37.30673 | -32.81660 | 50.79394 | -42.79907
16 | 13.53053 | -13.09007 | 25.85006 | -23.87095 | 39.42526 | -34.93408 | 53.61541 | -45.61998
17 | 14.20662 | -13.76202 | 27.25976 | -25.27856 | 41.54407 | -37.05199 | 56.43762 | -48.44172
18 | 14.88428 | -14.43590 | 28.66983 | -26.68685 | 43.66311 | -39.17025 | 59.26045 | -51.26415
19 | 15.56346 | -15.11164 | 30.08024 | -28.09571 | 45.78234 | -41.28883 | 62.08381 | -54.08717
20 | 16.24410 | -15.78913 | 31.49094 | -29.50506 | 47.90176 | -43.40767 | 64.90764 | -56.91070
21 | 16.92612 | -16.46828 | 32.90191 | -30.91485 | 50.02133 | -45.52674 | 67.73186 | -59.73467
Figure 5: Plots of the energy of KG oscillator for different values of
$\Omega$ with the parameters $K=0$ and $j=m=\omega=1,\varOmega\neq 0\;\ell=1.$