A class of toposes is introduced and studied, suitable for semantical analysis of an extension of the Heyting predicate calculus admitting Gödel's provability interpretation.

In a previous paper, an elementary and thoroughly arithmetical proof of Fermat’s last theorem by induction has been demonstrated if the case for “n = 3” is granted as proved only arithmetically (which is a fact a long time ago), furthermore in a way accessible to Fermat himself though without being absolutely and precisely correct. The present paper elucidates the contemporary mathematical background, from which an inductive proof of FLT can be inferred since its proof for the case for “n (...) = 3” has been known for a long time. It needs “Hilbert mathematics”, which is inherently complete unlike the usual “Gödel mathematics”, and based on “Hilbert arithmetic” to generalize Peano arithmetic in a way to unify it with the qubit Hilbert space of quantum information. An “epoché to infinity” (similar to Husserl’s “epoché to reality”) is necessary to map Hilbert arithmetic into Peano arithmetic in order to be relevant to Fermat’s age. Furthermore, the two linked semigroups originating from addition and multiplication and from the Peano axioms in the final analysis can be postulated algebraically as independent of each other in a “Hamilton” modification of arithmetic supposedly equivalent to Peano arithmetic. The inductive proof of FLT can be deduced absolutely precisely in that Hamilton arithmetic and the pransfered as a corollary in the standard Peano arithmetic furthermore in a way accessible in Fermat’s epoch and thus, to himself in principle. A future, second part of the paper is outlined, getting directed to an eventual proof of the case “n=3” based on the qubit Hilbert space and the Kochen-Specker theorem inferable from it. (shrink)

We consider formal theories synonymous with various free categories . Their Lindenbaum algebras may be described as the lattices of subobjects of a terminator. These theories have intuitionistic logic. We show that the Lindenbaum algebras of second order and higher order arithmetic , and set theory are not isomorphic to the Lindenbaum algebras of first order theories such as arithmetic . We also show that there are only five kernels of representations of the free Heyting algebra on one generator in (...) these Lindenbaum algebras. (shrink)

This is an expository paper on the problem of independent axiomatization of any set of sentences. This subject was investigated in 50's and 60's, and was abandoned later on, though not all fundamental questions were settled then. Besides, some papers written at that time are hardly available today and there are mistakes and misunderstandings there. We would like to get back to that unfinished business to clarify the subject matter, correct mistakes and answer questions left open by others. We shall (...) deal with results of many authors. However, they will be exposed in a different manner, with complete proofs and, often, with refinements and supplements. Some questions will be brought up to date and related to other questions in logic. New results and questions will also be added. Stress will be laid on constructive aspects; that is, we will examine the problem of the possibility of independent axiomatization as well as algebraic means by use of which independent sets of axioms can be given. (shrink)

We give a proof, valid in any elementary topos, of the theorem of Zermelo that any set possessing a choice function for its set of inhabited subsets can be well-ordered. Our proof is considerably simpler than existing proofs in the literature and moreover can be seen as a direct generalization of Zermelo's own 1908 proof of his theorem.