Online research in philosophy

We prove an institutional version of A. Robinson's Consistency Theorem. This result is then applied to the institution of many-sorted first-order predicate logic and to two of its variations, infinitary and partial, obtaining very general syntactic criteria sufficient for a signature square in order to satisfy the Robinson consistency and Craig interpolation properties.

We study prefixed tableaux for first-order multi-modal logic, providing proofs for soundness and completeness theorems, a Herbrand theorem on deductions describing the use of Herbrand or Skolem terms in place of parameters in proofs, and a lifting theorem describing the use of variables and constraints to describe instantiation. The general development applies uniformly across a range of regimes for defining modal operators and relating them to one another; we also consider certain simplifications that are possible with restricted modal theories and fragments.

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.

Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator ex. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.

Herbrand’s theorem is a central fact about classical logic, [9, 10]. It provides a constructive method for associating, with each first-order formula X, a sequence of formulas X1, X2, X3, . . . , so that X has a first-order proof if and only if some Xi is a tautology. Herbrand’s theorem serves as a constructive alternative to..

Modifying the methods of Z. Adamowicz's paper Herbrand consistency and bounded arithmetic [3] we show that there exists a number n such that ⋃m Sm (the union of the bounded arithmetic theories Sm) does not prove the Herbrand consistency of the finitely axiomatizable theory $S_{3}^{n}$.

On September 6, 2004, using the Isabelle proof assistant, I verified the following statement: (%x. pi x * ln (real x) / (real x)) ----> 1 The system thereby confirmed that the prime number theorem is a consequence of the axioms of higher-order logic together with an axiom asserting the existence of an infinite set. All told, our number theory session, including the proof of the prime number theorem and supporting libraries, constitutes 673 pages of proof scripts, or roughly 30,000 lines. This count includes about 65 pages of elementary number theory that we had at the outset, developed by Larry Paulson and others; also about 50 pages devoted to a proof of the law of quadratic reciprocity and properties of Euler’s ϕ function, neither of which are used in the proof of the prime number theorem. The page count does not include the basic HOL library, or properties of the real numbers that we obtained from the HOL-Complex library.