Hubbry Logo
Axiom schemaAxiom schemaMain
Open search
Axiom schema
Community hub
Axiom schema
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Axiom schema
Axiom schema
Axiom schema
View on Wikipedia
from Wikipedia

In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom.

Formal definition

[edit]

An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which may or may not be required to satisfy certain conditions. Often, such conditions require that certain variables be free, or that certain variables not appear in the subformula or term[citation needed].

Examples

[edit]

Two well known instances of axiom schemata are the:

Czesław Ryll-Nardzewski proved that Peano arithmetic cannot be finitely axiomatized, and Richard Montague proved that ZFC cannot be finitely axiomatized.[1][2] Hence, the axiom schemata cannot be eliminated from these theories. This is also the case for quite a few other axiomatic theories in mathematics, philosophy, linguistics, etc.

Finite axiomatization

[edit]

Given that the number of possible subformulas or terms that can be inserted in place of a schematic variable is infinite, an axiom schema stands for an infinite class or set of axioms. This set can often be defined recursively. A theory that can be axiomatized without schemata is said to be finitely axiomatizable.

Finitely axiomatized theories

[edit]

All theorems of ZFC are also theorems of von Neumann–Bernays–Gödel set theory, but the latter can be finitely axiomatized. The set theory New Foundations can be finitely axiomatized through the notion of stratification.

In higher-order logic

[edit]

Schematic variables in first-order logic are usually trivially eliminable in second-order logic, because a schematic variable is often a placeholder for any property or relation over the individuals of the theory. This is the case with the schemata of Induction and Replacement mentioned above. Higher-order logic allows quantified variables to range over all possible properties or relations.

See also

[edit]

Notes

[edit]

References

[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Axiom schema

View on Grokipedia
from Grokipedia
In , an is a formal template or formula expressed in the of an , containing one or more schematic variables (placeholders) that can be substituted with arbitrary well-formed formulas from the object language to generate an infinite collection of specific axioms. This approach allows for the concise definition of theories that require infinitely many axioms, avoiding the impracticality of listing them individually. Axiom schemata play a foundational role in formal systems such as propositional calculus, , and various mathematical theories, where they serve to axiomatize principles that apply universally across instances. For instance, in Peano arithmetic, the axiom schema of states that for any ϕ(x)\phi(x), if ϕ(0)\phi(0) holds and ϕ(n)\phi(n) implies ϕ(n+1)\phi(n+1) for all natural numbers nn, then ϕ(k)\phi(k) holds for all natural numbers kk; this schema yields one axiom per possible ϕ\phi, ensuring the completeness of the natural numbers under recursive definitions. In , particularly Zermelo-Fraenkel (ZF), the axiom schema of replacement asserts that for any set AA and any functional ϕ(x,y)\phi(x, y), the image of AA under ϕ\phi forms a set, enabling the construction of sets via transfinite and supporting the theory's expressive power for ordinals and cardinals. Similarly, the axiom schema of specification (or separation) in ZF allows the formation of subsets defined by any property within an existing set, preventing paradoxes while facilitating set comprehension. These schemata differ from finite axioms or second-order quantifiers by operating syntactically at the metalevel, with substitution rules ensuring that only valid instances are produced, often integrated with inference rules like uniform substitution to maintain deductive soundness. Their use underscores a key distinction in logic: axiom schemata provide a approximation to stronger infinitary principles, balancing expressiveness with finitary proof systems.

Definition and Purpose

Formal Definition

In , an is defined as a finite syntactic template or rule that generates an infinite collection of instances through the substitution of metavariables with appropriate well-formed formulas (wffs) or terms in the object language of a . This approach allows for the compact specification of sets that would otherwise require an infinite explicit listing, with each generated instance serving as a valid logical within the . The syntactic structure of an axiom schema consists of a schema formula expressed in the metalanguage, incorporating metavariables as placeholders for elements of the object language. Metavariables typically include symbols such as ϕ,ψ,χ\phi, \psi, \chi for arbitrary wffs, x,yx, y for individual variables, and tt for terms, with restrictions to ensure syntactic well-formedness (e.g., tt must be free for substitution in place of xx). Substitution rules mandate uniform replacement of these metavariables across the schema, avoiding variable capture where a substituted term's free variables become bound by quantifiers in the context. For instance, the general form of a schema can be denoted as ϕ(α1,…,αn)\phi(\alpha_1, \dots, \alpha_n), where ϕ\phi is the template formula and the αi\alpha_i are metavariables; an instance is obtained by substituting specific wffs or terms for each αi\alpha_i simultaneously, yielding a concrete axiom like ∀x ϕ(x)→ϕ(t)\forall x \, \phi(x) \to \phi(t) when ϕ\phi involves a unary metavariable. Axiom schemata differ from axiom schemes in that schemata emphasize the rule-based template itself, while schemes may refer to the resulting of instances; however, the terms are often used interchangeably in the to describe such generative mechanisms. Key properties include the fact that the is not itself a single or in the object but a meta-rule enabling recursive or iterative generation of axioms, ensuring each instance upholds logical validity without redundancy. This generative process supports the deductive completeness of systems like propositional and predicate calculi by producing all necessary tautologies or valid sentences as axioms or derivable theorems.

Motivation and Advantages

Axiom schemata are employed in formal systems to provide a finite means of expressing infinitely many axioms that capture general principles applicable across unbounded domains, such as the inductive properties of natural numbers or the comprehension of definable subsets in . This approach addresses the impracticality of enumerating all instances explicitly, allowing logicians to formalize uniform rules that hold for arbitrary formulas without resorting to higher-order quantification, which would otherwise inflate the ontological commitments of the theory. Historically, the adoption of axiom schemata arose in the early amid efforts to rigorize mathematical foundations and resolve paradoxes in and arithmetic. In 1908, introduced the axiom schema of separation in his axiomatization of to restrict unrestricted comprehension, which had led to contradictions like , by permitting the formation of subsets defined by any "definite" property within an existing set. Similarly, Giuseppe Peano's 1889 formulation of arithmetic evolved into first-order versions using an induction schema to encapsulate the principle of for all properties, avoiding the second-order quantification of the original while preserving expressive power. John von Neumann's 1927 axiomatization of propositional calculus further popularized schemata by replacing cumbersome finite axiom sets combined with substitution rules—prone to errors and complexity—with schema-based presentations that streamlined logical derivations. The primary advantages of axiom schemata include their compactness, enabling a finite description of theories with potentially infinite axiom sets, which supports recursive enumerability in standard systems and facilitates automated proof search and meta-theoretic investigations like completeness and consistency proofs. This structure enhances the practicality of formal systems for and applications, such as provers, by reducing the descriptive overhead while maintaining full generality. Although schemata can, in non-standard or higher-order contexts, generate non-recursively enumerable axiom sets that complicate decidability, their benefits in expressive power and foundational clarity generally outweigh these challenges in most axiomatic frameworks.

Examples in Logical Systems

Propositional and First-Order Logic

In propositional logic, axiom schemata provide an infinite set of axioms by allowing uniform substitution of well-formed formulas for metavariables, ensuring that all instances of tautologies can be derived within Hilbert-style proof systems. One common approach is the tautology schema, where every substitution instance of a propositional tautology serves as an axiom; however, more economical formulations use a finite set of schemata that generate all tautologies via modus ponens. A foundational example is the implication schema: ϕ→(ψ→ϕ)\phi \to (\psi \to \phi) where ϕ\phi and ψ\psi are metavariables replaced by any propositional formulas, such as p→(q→p)p \to (q \to p). Substitution here requires consistent replacement across all occurrences of a metavariable to preserve well-formedness, avoiding issues like mismatched connectives. Additional schemata, such as the distribution schema (ϕ→(ψ→χ))→((ϕ→ψ)→(ϕ→χ))(\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi)) and the contraposition schema (¬ψ→¬ϕ)→(ϕ→ψ),(\neg \psi \to \neg \phi) \to (\phi \to \psi), complete a minimal set for classical propositional logic, enabling derivations of all valid implications and negations. For instance, to derive the tautology ϕ→ϕ\phi \to \phi using these schemata and (from α\alpha and α→β\alpha \to \beta, infer β\beta), start with the instance (ϕ→((ϕ→ϕ)→ϕ))→((ϕ→(ϕ→ϕ))→(ϕ→ϕ))(\phi \to ((\phi \to \phi) \to \phi)) \to ((\phi \to (\phi \to \phi)) \to (\phi \to \phi)) from the distribution schema, combined with ϕ→((ϕ→ϕ)→ϕ)\phi \to ((\phi \to \phi) \to \phi) from the implication schema and ϕ→(ϕ→ϕ)\phi \to (\phi \to \phi) (another implication instance), yielding the desired result after applications of . These schemata form the propositional core of Hilbert systems, allowing compact axiomatization while covering infinitely many cases through substitution. In , axiom schemata extend propositional ones by incorporating quantifiers and terms, with substitution adapted to handle free variables and avoid capture under binders. The generalization axiom schema, also known as , states: ∀x ϕ(x)→ϕ(t)\forall x \, \phi(x) \to \phi(t) where tt is a term substitutable for xx in ϕ\phi, meaning xx does not become bound in ϕ(t)\phi(t) after replacement (e.g., no variable in tt is captured by a quantifier in ϕ\phi). Substitution ϕ[x/t]\phi[x/t] replaces free occurrences of xx with tt; for quantified formulas, if the quantifier binds xx, it remains unchanged (e.g., (∀x P(x))[y/c]=∀x P(x)(\forall x \, P(x))[y/c] = \forall x \, P(x) if y≠xy \neq x), but for unbound xx, it applies recursively (e.g., (∀y P(x))[x/c]=∀y P(c)(\forall y \, P(x))[x/c] = \forall y \, P(c)). Equality in first-order logic is axiomatized via schemata treating == as a binary predicate. The reflexivity schema is: ∀x (x=x),\forall x \, (x = x), ensuring every term equals itself. Substitutivity schemata allow replacement of equals: for functions, (x=y)→(f(…,x,… )=f(…,y,… )),(x = y) \to (f(\dots, x, \dots) = f(\dots, y, \dots)), and for atomic formulas, (x=y)→(ϕ(x)→ϕ(y)),(x = y) \to (\phi(x) \to \phi(y)), where ϕ(y)\phi(y) results from replacing some free xx with yy, preserving freeness. These extend to relations and ensure congruence. A simple derivation using the generalization schema: from ∀x (P(x)→P(x))\forall x \, (P(x) \to P(x)) (a propositional tautology generalized), instantiate with term tt to get P(t)→P(t)P(t) \to P(t), illustrating how schemata bridge propositional and predicate levels in Hilbert systems. Together, these schemata provide the foundational axioms for sound and complete proof systems in classical .

Arithmetic and Set Theory

In Peano arithmetic, a first-order theory formalizing the natural numbers, the axiom schema of induction serves as the primary mechanism for capturing mathematical induction over arbitrary definable properties of numbers. The schema posits that for every formula ϕ(n)\phi(n) in the language of arithmetic (which includes symbols for zero, successor, addition, and multiplication), the following holds: ϕ(0)∧∀n (ϕ(n)→ϕ(n+1))→∀n ϕ(n).\phi(0) \land \forall n \, (\phi(n) \to \phi(n+1)) \to \forall n \, \phi(n). This generates an infinite family of axioms, one for each possible ϕ\phi, ensuring that any property provably holding for 0 and preserved under the successor operation extends to all natural numbers. The schema is essential because the language admits infinitely many formulas, allowing the theory to axiomatize induction without second-order quantification, as in Peano's original second-order formulation. By parameterizing over all definable ϕ\phi, it enables the derivation of theorems about the entire infinite domain of natural numbers from a finite axiomatic base. In Zermelo-Fraenkel (ZF), the axiom schema of separation (also called restricted comprehension) facilitates the construction of subsets defined by arbitrary properties within existing sets, avoiding the paradoxes of unrestricted comprehension. For any existing set zz and any formula ϕ(x)\phi(x) in the language of set theory (with no free occurrences of yy), the schema asserts the existence of a set yy such that ∀x (x∈y↔x∈z∧ϕ(x)).\forall x \, (x \in y \leftrightarrow x \in z \land \phi(x)). Introduced by in his 1908 axiomatization, this produces infinitely many axioms, one per formula ϕ\phi, by restricting new sets to subsets of given ones, thus ensuring consistency while permitting sets via any definable relative to a prior set. A related , replacement, extends ZF's expressive power: for any set aa and formula ϕ(x,y)\phi(x, y) expressing a functional mapping (i.e., ∀x∃!y ϕ(x,y)\forall x \exists ! y \, \phi(x, y)), there exists a set bb containing the images {y∣∃x∈a ϕ(x,y)}\{ y \mid \exists x \in a \, \phi(x, y) \}. Proposed by Abraham Fraenkel in 1922 to address limitations in constructing infinite sequences and ordinals, replacement generates axioms for each such functional ϕ\phi, allowing the theory to build complex hierarchical structures like the von Neumann hierarchy from definable operations on existing sets. These schemata in arithmetic and exemplify the utility of in mathematical foundations, as they instantiate infinitely many specific from a finite template, thereby supporting proofs of boundless theorems—such as the infinitude of primes in Peano arithmetic or the of uncountable sets in ZF—while maintaining a compact axiomatic framework.

Finite Axiomatization

Infinite Sets of Axioms

Axiom schemata generate denumerably infinite sets of axioms, with one axiom produced for each substitution instance allowable in the theory's , due to the countably infinite number of well-formed formulas in standard formal . This infinity arises because schemata serve as templates that instantiate axioms systematically across all relevant , ensuring the theory captures general principles without enumerating them finitely. In , the quantifier axiom schemata exemplify this, yielding infinitely many axioms by substituting arbitrary formulas for schematic variables in axioms governing universal and existential quantification. Similarly, in Peano arithmetic, the induction schema produces one axiom for each formula, formalizing the principle of across all definable properties of natural numbers. These infinite axiom sets introduce significant theoretical challenges concerning decidability, completeness, and theorem enumerability. Decidability is typically lost in expressive theories incorporating such schemata, as the infinite axioms enable encoding of computations that outstrip effective decision procedures. Regarding completeness, Gödel's first incompleteness theorem demonstrates that recursively axiomatizable theories strong enough to interpret arithmetic—often relying on schemata like induction—are incomplete, containing true but unprovable statements within their own language. Theorem enumerability, however, remains feasible if the schema is recursive, allowing the axioms to be listed algorithmically. Theories employing recursive axiom schemata are recursively axiomatizable, meaning their axiom sets are recursively enumerable, which facilitates the semi-decidable generation of all provable theorems via standard proof systems. This property underpins the applicability of meta-logical results like Gödel's theorems to such systems, as the recursive nature ensures the theory's consistency and strength can be analyzed computably up to the limits of incompleteness.

Strategies for Finite Presentation

Strategies for finite presentation of theories relying on axiom schemata involve replacing the infinite collection of instances with a finite set of meta-axioms or by modifying the inference rules to capture the schema's effect without generating infinitely many axioms. One approach treats metavariables in the schema as primitive variables within an extended language, allowing a of axioms and substitution rules to derive all instances of the original . For instance, in formalizing predicate calculus, generalization rules—extending to —enable a finite axiomatization that avoids explicit schemata. In arithmetic, , denoted , exemplifies a finite axiomatization by omitting the full induction and using a weakened set of seven axioms for successor, , and , sufficient to represent computable functions yet avoiding the infinity of Peano arithmetic's induction instances. , the theory of natural numbers with but without , employs finite basic axioms alongside an induction restricted to addition-definable formulas, weakening the full while maintaining decidability, though the schema remains infinite. These examples illustrate how truncating or limiting schemata can lead to finite or more manageable presentations, as explored in early undecidability studies. The compactness theorem underpins key results in this area, stating that a theory has a model if and only if every finite subset does, which facilitates proofs of non-finite axiomatizability by constructing models satisfying finite axiom subsets but falsifying the full schema. This theorem highlights how infinite schemata ensure completeness for infinite domains, as finite approximations cannot capture all instances without gaps. Hilbert's program, aiming for a finitistic consistency proof of mathematics via a complete axiomatic basis, further influenced efforts to seek finite replacements for schemata, emphasizing contentual methods to justify infinite derivations from finite means. Despite these strategies, limitations persist: not all schema-based theories admit finite axiomatizations. Full Peano arithmetic, for example, requires the infinite induction schema and cannot be equivalently captured by any of first-order axioms, as proven using nonstandard models that satisfy finite subsets but violate the full theory. Such results underscore that while weakened schemata enable finite presentations in restricted theories like , stronger systems demand infinitary elements to fully axiomatize their intended models.

Extensions to Advanced Logics

Higher-Order Logic

In , axiom schemata are adapted to accommodate quantification over predicates, functions, and higher-type entities, extending beyond the individual variables of . A key adaptation is the higher-order rule, which allows inference from a ϕ(xα)\phi(\mathbf{x}_\alpha) (with xα\mathbf{x}_\alpha not free) to ∀Xα→oϕ(Xα→o)\forall X_{\alpha \to o} \phi(X_{\alpha \to o}), where Xα→oX_{\alpha \to o} is a variable of function type from α\alpha to propositions; this contrasts with by applying to predicate variables, generating more complex instances that capture relational properties. Another fundamental schema is the comprehension , which posits the existence of relations or functions defined by arbitrary formulas: ∃Rα1…αn→o∀x1α1…xnαn(R(x1,…,xn)↔ϕ(x1,…,xn))\exists R_{\alpha_1 \dots \alpha_n \to o} \forall x_1^{\alpha_1} \dots x_n^{\alpha_n} (R(x_1, \dots, x_n) \leftrightarrow \phi(x_1, \dots, x_n)), where ϕ\phi may include bound occurrences of RR, rendering it impredicative and enabling self-referential definitions essential for expressive power. Specific examples appear in simple type theory, such as Church's formulation, where schemata include extensionality axioms stating that entities of the same type are identical if they agree on all arguments—for propositional types, (X≡Y)⊃(X=Y)(X \equiv Y) \supset (X = Y), and for functional types, ∀xβ(fxβ=gxβ)⊃(f=g)\forall x_\beta (f x_\beta = g x_\beta) \supset (f = g)—ensuring that functions and predicates are identified by their extensions. Lambda abstraction schemata further support comprehension by allowing terms like λxα.ϕ(xα)\lambda x_\alpha . \phi(x_\alpha) to denote functions, which, when combined with the abstraction rule, generate axioms for higher-order operations without explicit set formation. These schemata handle predicate variables directly, differing from first-order logic by permitting quantification over the full hierarchy of types, which introduces impredicativity issues like potential circularity in definitions but enhances the ability to formalize mathematical concepts such as the continuum hypothesis. In applications, such as Church's simple theory of types, these schemata underpin the system's completeness: the axioms and rules, including and , yield a deductively complete system relative to general (Henkin) models, where comprehension is satisfied non-standardly to avoid incompleteness in full semantics. This framework formalizes classical while providing a typed foundation for , distinguishing it from untyped by preventing paradoxes through type restrictions.

Non-Classical and Alternative Systems

In , axiom schemata are formulated to exclude principles like the (A∨¬AA \vee \neg A) and elimination (¬¬A→A\neg \neg A \to A), ensuring that proofs constructively establish truth rather than assuming it classically. The propositional fragment (Heyting's intuitionistic propositional calculus, H–IPC) employs schemata such as A→(B→A)A \to (B \to A), (A→B)→((A→(B→C))→(A→C))(A \to B) \to ((A \to (B \to C)) \to (A \to C)), and A→(A∨B)A \to (A \vee B), alongside modus ponens, which mirror classical implicational and disjunctive axioms but reject ex falso quodlibet in its full classical strength without additional constraints. In first-order (H–IQC), quantifier schemata include ∀xA(x)→A(t)\forall x A(x) \to A(t) and A(t)→∃xA(x)A(t) \to \exists x A(x), with rules for universal introduction and existential elimination, but limited induction in systems like Heyting arithmetic takes the form (A(0)∧∀x(A(x)→A(S(x))))→∀xA(x)(A(0) \land \forall x (A(x) \to A(S(x)))) \to \forall x A(x), avoiding non-constructive instances that rely on excluded middle. Kripke semantics, using partially ordered frames with monotonically increasing domains, validates these schemata by requiring formulas to hold in all future worlds once true, implying that intuitionistic schemata capture persistent, constructive validity without classical bivalence. Modal logics extend axiom schemata to incorporate necessity (□\Box) and possibility (◊\Diamond), where basic systems like K use propositional schemata such as □(A→B)→(□A→□B)\Box(A \to B) \to (\Box A \to \Box B), but quantified variants add necessity schemata like □A→A\Box A \to A (reflexivity axiom M or T) to ensure necessary truths are actual. The Barcan formula schema, ∀x□A(x)→□∀xA(x)\forall x \Box A(x) \to \Box \forall x A(x), introduced by Ruth Barcan Marcus, holds in fixed-domain semantics where the domain of possible objects is constant across worlds, preventing the introduction of new existential commitments under necessity. Its converse, □∀xA(x)→∀x□A(x)\Box \forall x A(x) \to \forall x \Box A(x), applies in varying-domain models with nested domains (smaller in accessible worlds), requiring schemata to respect domain inclusions for non-classical validity in epistemic or metaphysical modalities. These schemata impose constraints on substitution, ensuring modal operators interact coherently with quantifiers without assuming classical existential generalization. In alternative systems like Martin-Löf dependent type theory, axiom schemata manifest as inference rules for dependent types, such as Pi-types (∏x:AB(x)\prod_{x:A} B(x)), which encode universal quantification intuitionistically via the propositions-as-types correspondence. The formation rule Γ⊢A  typeΓ,x:A⊢B(x)  typeΓ⊢∏x:AB(x)  type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}} allows types to depend on prior terms, with introduction via lambda abstraction and elimination by application, respecting non-classical validity through normalization and canonicity rather than classical deduction theorems. Fuzzy logics, such as basic logic (BL) by Petr Hájek, adjust schemata for truth degrees in [0,1], including (ϕ→ψ)→((ψ→χ)→(ϕ→χ))(\phi \to \psi) \to ((\psi \to \chi) \to (\phi \to \chi)) and ϕ&(ϕ→ψ)→ψ&(ψ→ϕ)\phi \& (\phi \to \psi) \to \psi \& (\psi \to \phi), but weaken classical tautologies like contraction to accommodate t-norm semantics, requiring instances to preserve residuated implications without bivalent sharpness. In relevance logics like R, schemata enforce variable-sharing, such as A→AA \to A (reflexivity) and distribution A→(B→(A∧B))A \to (B \to (A \land B)), with adjusted substitution rules that block irrelevant implications (e.g., no proof of (p∧¬p)→q(p \land \neg p) \to q without shared variables), validated by Routley-Meyer ternary relations to ensure premises contribute to conclusions. Across these systems, schemata incorporate additional constraints, like monotonicity in Kripke frames or domain stability in modals, to align with non-classical notions of validity such as constructivity or graded truth.

References

  1. https://plato.stanford.edu/entries/schema/
  2. https://mathworld.wolfram.com/AxiomSchema.html
  3. https://plato.stanford.edu/entries/set-theory/zf.html
  4. https://www.karlin.mff.cuni.cz/~krajicek/mendelson.pdf
  5. https://people.umass.edu/klement/514/ln.pdf
  6. https://planetmath.org/logicalaxiom
  7. https://plato.stanford.edu/entries/zermelo-set-theory/
  8. https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/schemata-the-concept-of-schema-in-the-history-of-logic/060A50DF9D5BD1C93D92C53B7F8FE211
  9. http://intrologic.stanford.edu/chapters/chapter_04.html
  10. https://people.math.ethz.ch/~halorenz/4students/LogikML/Nutshell.pdf
  11. https://ai.stanford.edu/~epacuit/classes/symblogic-fall2012/fol-notes.pdf
  12. http://user.math.uzh.ch/vorlesungen/mat115/hs17/web/RecapSheet_First_Order_Logic.pdf
  13. http://logic.stanford.edu/intrologic/extras/equality.html
  14. https://ocw.mit.edu/courses/24-242-logic-ii-spring-2004/2ba966be09dd1301d41d98be9276f3d1_peano_arithmetic.pdf
  15. https://plato.stanford.edu/entries/philosophy-mathematics/
  16. https://plato.stanford.edu/entries/goedel-incompleteness/
  17. https://planetmath.org/recursivelyaxiomatizabletheory
  18. https://us.metamath.org/downloads/finiteaxiom.pdf
  19. https://www.cs.cornell.edu/courses/cs4860/2012fa/lec-20.pdf
  20. https://iep.utm.edu/compactness/
  21. https://plato.stanford.edu/entries/hilbert-program/
  22. https://diposit.ub.edu/dspace/bitstream/2445/176007/2/176007.pdf
  23. https://plato.stanford.edu/entries/type-theory-church/
  24. https://plato.stanford.edu/entries/logic-higher-order/
  25. https://www.jstor.org/stable/2266967
  26. https://www.jstor.org/stable/2266170
  27. https://plato.stanford.edu/entries/logic-intuitionistic/
  28. https://plato.stanford.edu/entries/logic-modal/
  29. https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
  30. https://www.iiia.csic.es/media/filer_public/85/f6/85f61015-f103-458f-a90b-4ba0ff7285e9/4773.pdf
  31. https://plato.stanford.edu/entries/logic-relevance/
Add your contribution
Related Hubs
User Avatar
No comments yet.