Image de couverture de livre

A New Overture to Classical Simple Type Theory, Ketonen-type Gentzen and Tableau Systems

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Miwa, Tadayoshi, Inoué, Takao
Format:	Preprint
Publié:	2026
Sujets:	Logic 03B38, 03F03
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Nontrivial single axiom schemata and their quasi-nontriviality of Leśniewski-Ishimoto's propositional ontology $\bf L_1$
par: Inoué, Takao, et autres
Publié: (2024)

The Compatibility of the Minimalist Foundation with Homotopy Type Theory
par: Contente, Michele, et autres
Publié: (2022)

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
par: Gylterud, Håkon Robbestad, et autres
Publié: (2020)

Examples and counterexamples of injective types
par: de Jong, Tom, et autres
Publié: (2026)

Tableau Proof Systems for Justification Logics
par: Ghari, Meghdad
Publié: (2014)

Univalent Material Set Theory
par: Gylterud, Håkon Robbestad, et autres
Publié: (2023)

Internal Effectful Forcing in System T
par: Escardo, Martin H., et autres
Publié: (2025)

Meaning as Use, Application, Employment, Purpose, Usefulness
par: de Queiroz, Ruy J. G. B.
Publié: (2025)

From the Notebooks to the Investigations and Beyond
par: de Queiroz, Ruy J. G. B.
Publié: (2025)

On the Various Translations between Classical, Intuitionistic and Linear Logic
par: Ferreira, Gilda, et autres
Publié: (2024)

Dependent Types Simplified
par: Bice, Tristan
Publié: (2025)

Type Theory with Explicit Universe Polymorphism (revised and extended version)
par: Bezem, Marc, et autres
Publié: (2022)

NF is Consistent
par: Holmes, M. Randall, et autres
Publié: (2015)

Hierarchical formula classes with respect to semi-classical prenex normalization
par: Fujiwara, Makoto, et autres
Publié: (2025)

Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
par: Lyon, Tim S.
Publié: (2025)

Intuitionistic Common Knowledge
par: Zenger, Lukas
Publié: (2026)

Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations
par: Ayhan, Sara
Publié: (2023)

Continuations and Completeness in Proof-theoretic Semantics
par: Gu, Tao, et autres
Publié: (2026)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
par: Farmer, William M., et autres
Publié: (2023)

Herbrandized modified realizability
par: Ferreira, Gilda, et autres
Publié: (2024)

A Deep-Inference Sequent Calculus for Basic Propositional Team Logic (Without Delving Too Deep)
par: Anttila, Aleksi, et autres
Publié: (2025)

Lewis and Brouwer meet Strong Löb
par: Visser, Albert, et autres
Publié: (2024)

Constructive proofs for the standard translation of many-sorted to unsorted predicate logic
par: Oddsson, Hrafn Valtýr
Publié: (2026)

Herbrand's Theorem: a short statement and a model-theoretic proof
par: Badano, Mariana
Publié: (2025)

Open questions about Ramsey-type statements in reverse mathematics
par: Patey, Ludovic
Publié: (2015)

Encoding Sequences in Intuitionistic Real Algebra
par: Erdélyi-Szabó, Miklós
Publié: (2025)

Generalized Kripke's Schema and the Expressive Power of Intuitionistic Real Algebra
par: Erdélyi-Szabó, Miklós
Publié: (2024)

A vector logic for extensional formal semantics
par: Quigley, Daniel
Publié: (2024)

Reduced Set Theory
par: Kunik, Matthias
Publié: (2023)

Avoiding logical strength in real analysis
par: Freund, Anton, et autres
Publié: (2026)

Cut-free sequent calculi for the provability logic D
par: Kashima, Ryo, et autres
Publié: (2023)

Weak and Strong Versions of Effective Transfinite Recursion
par: Uftring, Patrick
Publié: (2022)

Proof-theoretic methods in quantifier-free definability
par: Kocsis, Zoltan A.
Publié: (2023)

Ketonen's question and other cardinal sins
par: Rinot, Assaf, et autres
Publié: (2024)

The Uniform Functional Interpretation with Informative Types
par: Ferreira, Fernando, et autres
Publié: (2025)

Kripke-Joyal forcing for type theory and uniform fibrations
par: Awodey, S., et autres
Publié: (2021)

On inverse Goodstein sequences
par: Uftring, Patrick
Publié: (2023)

Induction on Dilators and Bachmann-Howard Fixed Points
par: Aguilera, Juan P., et autres
Publié: (2024)

Algorithmic correspondence and analytic rules
par: De Domenico, Andrea, et autres
Publié: (2022)

Labeled Sequent Calculus and Countermodel Construction for Justification Logics
par: Ghari, Meghdad
Publié: (2014)