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

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

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Axiom of Choice and Complementation
• Hilbert's ϵ‐operator in intuitionistic type theories
• Epsilon substitution for first- and second-order predicate logic
• 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)