On the semantics of the universal quantifier

DOI10.1016/S0168-0072(96)00051-6MaRDI QIDQ1371430zbMATH OpenFDO

Authors Djordje Čubrić

Publication date 23 February 1998

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0168-0072(96)00051-6

zbMATH Keywords

categorical semanticscompleteness theoremsfibrationsfragment of intuitionistic logicproof theoryYoneda embedding

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Proof theory in general (including proof-theoretic semantics) (03F03) Categorical logic, topoi (03G30) Fibered categories (18D30)

Review text

The author studies the proof theory and categorical semantics of the \((\top,\wedge,\to,\forall)\) fragment of intuitionistic logic, using a class of fibrations which he calls \(\forall\)-fibrations to provide the models. The key observation which makes it easy to prove completeness theorems for this fragment is that the above connectives are precisely those whose interpretations are preserved by the Yoneda embedding (when they exist).

Recommendations

• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
• Quantifier-complete categories
• Algebra of proofs
• A simplified semantics for a fragment of intuitionistic linear logic

Cites work

• Adjointness in Foundations
• An application of open maps to categorical logic
• Categories for Types
• Fibered categories and the foundations of naive category theory
• Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 4049849 (Why is no real title available?)
• scientific article; zbMATH DE number 130889 (Why is no real title available?)
• scientific article; zbMATH DE number 3485758 (Why is no real title available?)
• scientific article; zbMATH DE number 3605078 (Why is no real title available?)
• scientific article; zbMATH DE number 512797 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Locally cartesian closed categories and type theory
• On the rules of suppositions in formal logic
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
• The virtues of eta-expansion
• Yoneda structures on 2-categories

Cited in

(7)

• Coherence in linear predicate logic
• On the definability of the quantifier there exist uncountably many
• On the ontology of branching quantifiers
• Discussion Note On: “Semantic Nominalism: How I Learned to Stop Worrying and Love Universals” by G. Aldo Antonelli
• On the Proper Treatment of Quantifiers in Montague Semantics
• All Quantifiers Versus the Quantifier All
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi

Describes a project that uses

Uses Software

• Automath

This page was built for publication: On the semantics of the universal quantifier

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