A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's -terms

DOI10.1007/S11787-016-0155-YMaRDI QIDQ528519zbMATH OpenOpenAlexFDO

Authors Fabio Pasquali

Publication date 12 May 2017

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-016-0155-y

zbMATH Keywords

categorical logicHilbert's epsilon calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Type theory (03B38)

Recommendations

• Hilbert's ϵ‐operator in intuitionistic type theories
• Epsilon Calculi
• Intuitionistic ϵ‐ and τ‐calculi
• Semantics and proof theory of the epsilon calculus
• Hilbert's \(\varepsilon{}\)-operator and classical logic

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3574077 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Axiom of Choice and Complementation
• Epsilon substitution for first- and second-order predicate logic
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Hilbert's ϵ‐operator in intuitionistic type theories
• The substitution method revisited

Cited in

(4)

• On a generalization of equilogical spaces
• Dialectica principles via Gödel doctrines
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus

This page was built for publication: A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's \(\varepsilon\)-terms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q528519)