Proposition algebra

DOI10.1145/1929954.1929958MaRDI QIDQ2946640zbMATH OpenOpenAlexFDO

Authors J. A. Bergstra, Alban Ponse

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0807.3648

zbMATH Keywords

conditional compositionpropositional statementreactive valuationsatisfiabilitysequential connectiveshort-circuit evaluationside effect

Mathematics Subject Classification ID

Logic in computer science (03B70) Other algebras related to logic (03G25) Abstract data types; algebraic specification (68Q65)

Abstract: Sequential propositional logic deviates from ordinary propositional logic by taking into account that during the sequential evaluation of a propositional statement,atomic propositions may yield different Boolean values at repeated occurrences. We introduce `free valuations' to capture this dynamics of a propositional statement's environment. The resulting logic is phrased as an equationally specified algebra rather than in the form of proof rules, and is named `proposition algebra'. It is strictly more general than Boolean algebra to the extent that the classical connectives fail to be expressively complete in the sequential case. The four axioms for free valuation congruence are then combined with other axioms in order define a few more valuation congruences that gradually identify more propositional statements, up to static valuation congruence (which is the setting of conventional propositional logic). Proposition algebra is developed in a fashion similar to the process algebra ACP and the program algebra PGA, via an algebraic specification which has a meaningful initial algebra for which a range of coarser congruences are considered important as well. In addition infinite objects (that is propositional statements, processes and programs respectively) are dealt with by means of an inverse limit construction which allows the transfer of knowledge concerning finite objects to facts about infinite ones while reducing all facts about infinite objects to an infinity of facts about finite ones in return.

Recommendations

• scientific article; zbMATH DE number 4031629
• Proposition algebra and short-circuit logic
• Algebra of proofs
• scientific article; zbMATH DE number 1059248
• scientific article; zbMATH DE number 823612
• scientific article; zbMATH DE number 4213954
• Proof theory and algebra in logic
• scientific article; zbMATH DE number 1852925
• scientific article; zbMATH DE number 3164639

Cited in

(9)

• Proposition algebra and short-circuit logic
• Evaluation trees for proposition algebra
• On a sequential model of the algebra of finite-valued logic
• Encoding many-valued logic in \lambda-calculus
• An independent axiomatisation for free short-circuit logic
• Non-commutative propositional logic with short-circuit evaluation
• Fully evaluated left-sequential logics
• Conditional logic as a short-circuit logic
• Logical models of mathematical texts. II: legality conventions for division by zero in inconsistent contexts

This page was built for publication: Proposition algebra

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