Online research in philosophy

In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.

With the past and future tense propositional operators in its syntax, a formal logical system for sortal quantifiers, sortal identity and (second order) quantification over sortal concepts is formulated. A completeness proof for the system is constructed and its absolute consistency proved. The completeness proof is given relative to a notion of logical validity provided by an intensional semantic system, which assumes an approach to sortals from a modern form of conceptualism.

In this paper the modal operator "x is provable in Peano Arithmetic" is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

In this paper the system IL for relative interpretability described in Visser (1988) is studied.1 In IL formulae A|> B (read: A interprets B) are added to the provability logic L. The intended interpretation of a formula A|> B in an (arithmetical) theory T is: T + B is relatively interpretable in T + A. The system has been shown to be sound with respect to such arithmetical interpretations (˘Svejdar 1983, Montagna 1984, Visser 1986, 1988P). As axioms for IL we take the usual axioms A→ A and ( A→A)→ A (Löb's Axiom) for the provability logic L and its rules, modus ponens and necessitation, plus the axioms: (1) (A→B)→(A|>B ) (2) (A|> B) ∧ (B|> C) → (A|> C) (3) (A|> C) ∧ (B|> C)→(A∨B|> C) (4) (A|> B)→( A→ B) (5) A|>A With respect to priority of parentheses |> is treated as →.

The system called F is essentially a sub-theory of Frege Arithmetic without the ad infinitum assumption that there is always a next number. In a series of papers (Systems for a Foundation of Arithmetic, True” Arithmetic Can Prove Its Own Consistency and Proving Quadratic Reciprocity) it was shown that F proves a large number of basic arithmetic truths, such as the Euclidean Algorithm, Unique Prime Factorization (i.e. the Fundamental Law of Arithmetic), and Quadratic Reciprocity, indeed a sizable amount of arithmetic. In particular, F proves some (but not all) of the Peano Axioms; that is, F proves the axioms of a sub-theory - call it FPA - of second-order Peano-Arithmetic. This short technical note will demonstrate that the converse also holds, in the following sense. F has the same language as second-order Peano Arithmetic except that, in addition, it has a two-place predicate symbol “Μ”. Then it is possible to provide a definition, indeed a reasonable definition, for “Μ” such that FPA proves all the axioms of F. So F and FPA effectively have the same proof-theoretic strength. In particular FPA, which lacks the Successor Axiom stating that every natural number has a successor, is able to prove the Euclidean Algorithm, Unique Prime Factorization, and Quadratic Reciprocity, indeed (again) a sizable amount of arithmetic.

In this paper the system IL for relative interpretability described in Visser (1988) is studied.1 In IL formulae A|> B (read: A interprets B) are added to the provability logic L. The intended interpretation of a formula A|.

The modal logic of Gödel sentences, termed as GS , is introduced to analyze the logical properties of ‘true but unprovable’ sentences in formal arithmetic. The logic GS is, in a sense, dual to Grzegorczyk’s Logic, where modality can be interpreted as ‘true and provable’. As we show, GS and Grzegorczyk’s Logic are, in fact, mutually embeddable. We prove Kripke completeness and arithmetical completeness for GS . GS is also an extended system of the logic of ‘Essence and Accident’ proposed by Marcos (Bull Sect Log 34(1):43–56, 2005 ). We also clarify the relationships between GS and the provability logic GL and between GS and Intuitionistic Propositional Logic.

It might seem that three of Godel’s results - the Completeness and the First and Second Incompleteness Theorems - assume so little that they are reasonably indisputable. A version of the Completeness Theorem, for instance, can be proven in RCA0, which is the weakest system studied extensively in Simpson’s encyclopaedic Subsystems of Second Order Arithmetic. And it often seems that the minimum requirements for a system just to express the Incompleteness Theorems are sufficient to prove them. However, it will be shown that a particular sub-system of Peano Arithmetic is powerful enough to express assertions about syntax, provability, consistency, and models, while being too weak to allow the standard proofs of the theorems to go through. An alternative proof is available for the First Incompleteness Theorem, but is of such a different nature that the import of the theorem changes. And there are no alternative proofs for (certainly) the Completeness and (apparently) the Second Incompleteness Theorems. It is therefore perfectly rational for someone to be skeptical about Godel’s results.

PA is Peano Arithmetic. Pr(x) is the usual Σ1-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬ Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness. In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications.

The paper presents a proof of the consistency of Peano Arithmetic (PA) that does not lie in deducing its consistency as a theorem in an axiomatic system. PA’s consistency cannot be proved in PA, and to deduce its consistency in some stronger system PA+ is self-defeating, since the stronger system may itself be inconsistent. Instead, a semantic proof is constructed which demonstrates consistency not relative to the consistency of some other system but in an absolute sense.