One-and-a-halfth-order Logic

DOI10.1093/logcom/exm064zbMath1158.03006OpenAlexW2062446527MaRDI QIDQ3520234

Aad Mathijssen, Murdoch James Gabbay

Publication date: 15 August 2008

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exm064

zbMATH Keywords

first-order logicsubstitutionnominal techniques\({\alpha}\)-conversionformalization of meta-variables

Mathematics Subject Classification ID

Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Algebraic logic (03G99)

Related Items (11)

Simple and subdirectly irreducible finitely supported \(Cb\)-sets ⋮ Presenting functors on many-sorted varieties and applications ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Unity in nominal equational reasoning: the algebra of equality on nominal sets ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness ⋮ Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets ⋮ A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets ⋮ Two-level Lambda-calculus ⋮ Nominal Equational Logic

This page was built for publication: One-and-a-halfth-order Logic