The Consistency Of A Variant Of Church's Thesis With An Axiomatic Theory Of An Epistemic Notion.
The creative subject and Heyting's arithmetic
The Dialectica interpretation of first-order classical affine logic.
The double powerlocale and exponentiation: A case study in geometric logic.
The Frobenius relations meet linear distributivity.
The Gödel Completeness Theorem for Uncountable Languages
This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.
The lattices of numerations of theories containing Peano's arithmetic
The limit lemma in fragments of arithmetic
The recursion theoretic limit lemma, saying that each function with a graph is a limit of certain function with a graph, is provable in .
The polynomial bounds of proof complexity in Frege systems.
The projective spectrum as a distributive lattice
The second isomorphism theorem on ordered set under antiorders
The strength of Turing determinacy within second order arithmetic
We investigate the reverse mathematical strength of Turing determinacy up to Σ₅⁰, which is itself not provable in second order arithmetic.
The "World's Simplest Axiom of Choice" Fails.
Theorem Provers for Substructural Logics
Three-valued logic and cut-elimination: The actual meaning of Takeuti's conjecture [Book]
Topological properties of the real numbers object in a topos
Transition of Consistency and Satisfiability under Language Extensions
This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.