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

DOI10.1007/S11787-016-0155-YzbMATH Open1436.03093OpenAlexW2524346107MaRDI QIDQ528519

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

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Epsilon substitution for first- and second-order predicate logic
• Axiom of Choice and Complementation
• Hilbert's ϵ‐operator in intuitionistic type theories

Related Items (4)

On a generalization of equilogical spaces ⋮ Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator ⋮ Dialectica principles via Gödel doctrines ⋮ 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