Permutability of rules in lattice theory.

DOI10.1007/S000120200012MaRDI QIDQ1771961zbMATH OpenOpenAlexFDO

Authors Sara Negri, Jan von Plato

Publication date 19 April 2005

Published in Algebra Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s000120200012

zbMATH Keywords

decidabilityderivability of universal formulaslattice theoryproof analysis

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Structure of proofs (03F07) Free lattices, projective lattices, word problems (06B25)

Review text

The main result is the so-called Subterm Property: If an atomic formula is derivable from given atomic formulas in lattice theory then it has a derivation all terms of which are terms in the given formulas or the conclusion. This has the following consequences: Lattice theory is conservative over partial order for universal formulas. The derivability of universal formulas in lattice theory is decidable.

Recommendations

• Permutability of rules for linear lattices
• Proof systems for lattice theory
• scientific article; zbMATH DE number 4037828
• Term rewrite systems for lattice theory
• scientific article; zbMATH DE number 1145524

Cited in

(7)

• The intensional side of algebraic-topological representation theorems
• A solution of the uniform word problem for ortholattices
• Proof systems for lattice theory
• Permutability of rules for linear lattices
• In the Shadows of the Löwenheim-Skolem Theorem: Early Combinatorial Analyses of Mathematical Proofs
• Combinatorial analysis of proofs in projective and affine geometry
• Decidability of lattice equations

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Permutability of rules in lattice theory.

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