Formalizing the meta-theory of first-order predicate logic

DOI10.4134/JKMS.J160546MaRDI QIDQ4609965zbMATH OpenOpenAlexFDO

Authors Hugo Herberlin, Sunyoung Kim, Gyesik Lee

Publication date 27 March 2018

Full work available at URL http://dspace.kci.go.kr/handle/kci/195260

zbMATH Keywords

completenessKripke semanticssoundnessfirst-order predicate logicformal proofs

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30)

Recommendations

• GMeta: a generic formal metatheory framework for first-order representations
• Some logical and syntactical observations concerning the first-order dependent type system λP
• Engineering formal metatheory
• Completeness theorems for first-order logic analysed in constructive type theory
• Types for Proofs and Programs

Cited in

(4)

• A linear logic framework for multimodal logics
• scientific article; zbMATH DE number 1754648 (Why is no real title available?)
• Formalized meta-theory of sequent calculi for substructural logics
• Adding metatheoretic facilities to first-order theories

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL

This page was built for publication: Formalizing the meta-theory of first-order predicate logic

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