Changes

<font size="3">&#9758;</font> This page belongs to resource collections on [[Logic Live|Logic]] and [[Inquiry Live|Inquiry]].

<font size="3">&#9758;</font> This page belongs to resource collections on [[Logic Live|Logic]] and [[Inquiry Live|Inquiry]].

A '''propositional calculus''' (or a '''sentential calculus''') is a [[formal system]] that represents the materials and the principles of ''propositional logic'' (or ''sentential logic'').  Propositional logic is a domain of formal subject matter that is, up to [[isomorphism]], constituted by the structural relationships of mathematical objects called ''[[proposition (mathematics)|proposition]]s''.

A '''propositional calculus''' (or a '''sentential calculus''') is a formal system that represents the materials and the principles of ''propositional logic'' (or ''sentential logic'').  Propositional logic is a domain of formal subject matter that is, up to somorphism, constituted by the structural relationships of mathematical objects called ''propositions''.

In general terms, a calculus is a [[formal system]] that consists of a set of syntactic expressions (''well-formed formulas'' or ''wffs''), a distinguished subset of these expressions, plus a set of transformation rules that define a [[binary relation]] on the space of expressions.   

In general terms, a calculus is a formal system that consists of a set of syntactic expressions (''well-formed formulas'' or ''wffs''), a distinguished subset of these expressions, plus a set of transformation rules that define a binary relation on the space of expressions.   

When the expressions are interpreted for mathematical purposes, the transformation rules are typically intended to preserve some type of [[semantic equivalence relation]] among the expressions.  In particular, when the expressions are interpreted as a [[logical system]], the [[semantic equivalence]] is typically intended to be [[logical equivalence]].  In this setting, the transformation rules can be used to derive logically equivalent expressions from any given expression.  These derivations include as special cases (1) the problem of ''simplifying'' expressions and (2) the problem of deciding whether a given expression is equivalent to an expression in the distinguished subset, typically interpreted as the subset of logical ''[[axiom]]s''.

When the expressions are interpreted for mathematical purposes, the transformation rules are typically intended to preserve some type of semantic equivalence relation among the expressions.  In particular, when the expressions are interpreted as a logical system, the semantic equivalence is typically intended to be logical equivalence.  In this setting, the transformation rules can be used to derive logically equivalent expressions from any given expression.  These derivations include as special cases (1) the problem of ''simplifying'' expressions and (2) the problem of deciding whether a given expression is equivalent to an expression in the distinguished subset, typically interpreted as the subset of logical ''axioms''.

The set of axioms may be empty, a nonempty finite set, a countably infinite set, or given by axiom schemata.  A [[formal grammar]] recursively defines the expressions and well-formed formulas (wffs) of the [[formal language|language]].  In addition a [[semantics]] is given which defines truth and valuations (or interpretations).  It allows us to determine which wffs are valid, that is, are [[theorem]]s.

The set of axioms may be empty, a nonempty finite set, a countably infinite set, or given by axiom schemata.  A formal grammar recursively defines the expressions and well-formed formulas (wffs) of the language.  In addition a semantics is given which defines truth and valuations (or interpretations).  It allows us to determine which wffs are valid, that is, are theorems.

The [[formal language|language]] of a propositional calculus consists of (1) a set of primitive symbols, variously referred to as ''atomic formulas'', ''placeholders'', ''proposition letters'', or ''variables'', and (2) a set of operator symbols, variously interpreted as ''[[logical operator]]s'' or ''[[logical connective]]s''.  A ''well-formed formula'' (''wff'') is any atomic formula or any formula that can be built up from atomic formulas by means of operator symbols.

The language of a propositional calculus consists of (1) a set of primitive symbols, variously referred to as ''atomic formulas'', ''placeholders'', ''proposition letters'', or ''variables'', and (2) a set of operator symbols, variously interpreted as ''logical operators'' or ''logical connectives''.  A ''well-formed formula'' (''wff'') is any atomic formula or any formula that can be built up from atomic formulas by means of operator symbols.

The following outlines a standard propositional calculus. Many different formulations exist which are all more or less equivalent but differ in (1) their language, that is, the particular collection of primitive symbols and operator symbols, (2) the set of axioms, or distingushed formulas, and (3) the set of transformation rules that are available.

The following outlines a standard propositional calculus. Many different formulations exist which are all more or less equivalent but differ in (1) their language, that is, the particular collection of primitive symbols and operator symbols, (2) the set of axioms, or distingushed formulas, and (3) the set of transformation rules that are available.

==Generic description of a propositional calculus==

==Generic description of a propositional calculus==

A '''propositional calculus''' is a [[formal system]] <math>\mathcal{L} = \mathcal{L}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota)</math>,  whose formulas are constructed in the following manner:

A '''propositional calculus''' is a formal system <math>\mathcal{L} = \mathcal{L}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota)</math>,  whose formulas are constructed in the following manner:

* The ''alpha set'' <math>\Alpha\!</math> is a finite set of elements called ''proposition symbols'' or ''[[propositional variable]]s''.  Syntactically speaking, these are the most basic elements of the formal language <math>\mathcal{L}</math>, otherwise referred to as ''[[atomic formula]]s'' or ''terminal elements''.  In the examples to follow, the elements of <math>\Alpha\!</math> are typically the letters ''p'', ''q'', ''r'', and so on.

* The ''alpha set'' <math>\Alpha\!</math> is a finite set of elements called ''proposition symbols'' or ''propositional variables''.  Syntactically speaking, these are the most basic elements of the formal language <math>\mathcal{L},</math> otherwise referred to as ''atomic formulas'' or ''terminal elements''.  In the examples to follow, the elements of <math>\Alpha\!</math> are typically the letters ''p'', ''q'', ''r'', and so on.

* The ''omega set'' <math>\Omega\!</math> is a finite set of elements called ''[[operator|operator symbols]]'' or ''[[logical connective]]s''.  The set <math>\Omega\!</math> is [[partition]]ed into disjoint subsets as follows:

* The ''omega set'' <math>\Omega\!</math> is a finite set of elements called ''operator symbols'' or ''logical connectives''.  The set <math>\Omega\!</math> is partitioned into disjoint subsets as follows:

: In this partition, <math>\Omega_j\!</math> is the set of operator symbols of ''arity'' <math>j.\!</math>

 

 

: In this partition, <math>\Omega_j\!</math> is the set of operator symbols of ''[[arity]]'' <math>j\!</math>.

: In the more familiar propositional calculi, <math>\Omega\!</math> is typically partitioned as follows:

: In the more familiar propositional calculi, <math>\Omega\!</math> is typically partitioned as follows:

::: <math>\Omega_1 = \{ \lnot \} \,,</math>

::: <math>\Omega_1 = \{ \lnot \},\!</math>

::: <math>\Omega_2 \subseteq \{ \land, \lor, \rightarrow, \leftrightarrow \} \,.</math>

::: <math>\Omega_2 \subseteq \{ \land, \lor, \rightarrow, \leftrightarrow \}.\!</math>

: A frequently adopted option treats the constant [[logical value]]s as operators of arity zero, thus:

: A frequently adopted option treats the constant logical values as operators of arity zero, thus:

::: <math>\Omega_0 = \{0,\ 1 \} \,.</math>

::: <math>\Omega_0 = \{ 0, 1 \}.\!</math>

: Some writers use the [[tilde]] (~) instead of (¬) and some use the [[ampersand]] (&) instead of (&#8743;).  Notation varies even more for the set of logical values, with symbols like {false, true}, {F, T}, {0, 1}, and {<math>\bot</math>, <math>\top</math>} all being seen in various contexts.

: Some writers use the tilde (~) instead of (¬) and some use the ampersand (&) instead of (&#8743;).  Notation varies even more for the set of logical values, with symbols like {false, true}, {F, T}, {0, 1}, and {<math>\bot</math>, <math>\top</math>} all being seen in various contexts.

* Depending on the precise formal grammar or the grammar formalism that is being used, syntactic auxiliaries like the left parenthesis, "(", and the right parentheses, ")", may be necessary to complete the construction of formulas.

* Depending on the precise formal grammar or the grammar formalism that is being used, syntactic auxiliaries like the left parenthesis, "(", and the right parentheses, ")", may be necessary to complete the construction of formulas.

The ''language'' of <math>\mathcal{L}</math>, also known as its set of ''formulas'', ''[[well-formed formula]]s'' or ''[[wff]]s'', is [[mathematical induction|inductively]] or [[recursive]]ly defined by the following rules:

The ''language'' of <math>\mathcal{L}</math>, also known as its set of ''formulas'', ''well-formed formulas'' or ''wffs'', is inductively or recursively defined by the following rules:

# Base.  Any element of the alpha set <math>\Alpha\!</math> is a formula of <math>\mathcal{L}</math>.

# Base.  Any element of the alpha set <math>\Alpha\!</math> is a formula of <math>\mathcal{L}</math>.

# By rule 3, (¬''p'' &#8744; ''q'') is a formula.

# By rule 3, (¬''p'' &#8744; ''q'') is a formula.

* The ''zeta set'' <math>\Zeta\!</math> is a finite set of ''transformation rules'' that are called ''[[inference rule]]s'' when they acquire logical applications.

* The ''zeta set'' <math>\Zeta\!</math> is a finite set of ''transformation rules'' that are called ''inference rules'' when they acquire logical applications.

* The ''iota set'' <math>\Iota\!</math> is a finite set of ''initial points'' that are called ''[[axiom]]s'' when they receive logical interpretations.

* The ''iota set'' <math>\Iota\!</math> is a finite set of ''initial points'' that are called ''axioms'' when they receive logical interpretations.

==Example 1.  Simple axiom system==

==Example 1.  Simple axiom system==

{{col-begin}}

{{col-begin}}

{{col-break}}

{{col-break}}

* [http://mywikibiz.com/Propositional_calculus Propositional Calculus @ MyWikiBiz]

* [http://mywikibiz.com/Propositional_calculus Propositional Calculus @ MyWikiBiz]

{{col-break}}

{{col-break}}

* [http://wiki.oercommons.org/mediawiki/index.php/Propositional_calculus Propositional Calculus @ OER Commons]

* [http://beta.wikiversity.org/wiki/Propositional_calculus Propositional Calculus @ Wikiversity Beta]

* [http://p2pfoundation.net/Propositional_Calculus Propositional Calculus @ P2P Foundation]

* [http://ref.subwiki.org/wiki/Propositional_calculus Propositional Calculus @ Subject Wikis]

* [http://semanticweb.org/wiki/Propositional_calculus Propositional Calculus @ SemanticWeb]

{{col-end}}

{{col-end}}

===Related articles===

===Related articles===

* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Semiotic_Information Jon Awbrey, &ldquo;Semiotic Information&rdquo;]

 

* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Introduction_to_Inquiry_Driven_Systems Jon Awbrey, &ldquo;Introduction To Inquiry Driven Systems&rdquo;]

* [http://intersci.ss.uci.edu/wiki/index.php/Cactus_Language Cactus Language]

 

* [http://intersci.ss.uci.edu/wiki/index.php/Futures_Of_Logical_Graphs Futures Of Logical Graphs]

* [http://mywikibiz.com/Directory:Jon_Awbrey/Essays/Prospects_For_Inquiry_Driven_Systems Jon Awbrey, &ldquo;Prospects For Inquiry Driven Systems&rdquo;]

* [http://intersci.ss.uci.edu/wiki/index.php/Propositional_Equation_Reasoning_Systems Propositional Equation Reasoning Systems]

 

* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Inquiry_Driven_Systems Jon Awbrey, &ldquo;Inquiry Driven Systems : Inquiry Into Inquiry&rdquo;]

* [http://intersci.ss.uci.edu/wiki/index.php/Differential_Logic_:_Introduction Differential Logic : Introduction]

 

* [http://intersci.ss.uci.edu/wiki/index.php/Differential_Propositional_Calculus Differential Propositional Calculus]

* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Propositional_Equation_Reasoning_Systems Jon Awbrey, &ldquo;Propositional Equation Reasoning Systems&rdquo;]

* [http://intersci.ss.uci.edu/wiki/index.php/Differential_Logic_and_Dynamic_Systems_2.0 Differential Logic and Dynamic Systems]

 

* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Differential_Logic_:_Introduction Jon Awbrey, &ldquo;Differential Logic : Introduction&rdquo;]

* [http://intersci.ss.uci.edu/wiki/index.php/Prospects_for_Inquiry_Driven_Systems Prospects for Inquiry Driven Systems]

 

* [http://intersci.ss.uci.edu/wiki/index.php/Introduction_to_Inquiry_Driven_Systems Introduction to Inquiry Driven Systems]

* [http://planetmath.org/encyclopedia/DifferentialPropositionalCalculus.html Jon Awbrey, &ldquo;Differential Propositional Calculus&rdquo;]

* [http://intersci.ss.uci.edu/wiki/index.php/Inquiry_Driven_Systems Inquiry Driven Systems : Inquiry Into Inquiry]

 

* [http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Differential_Logic_and_Dynamic_Systems_2.0 Jon Awbrey, &ldquo;Differential Logic and Dynamic Systems&rdquo;]

==Document history==

==Document history==

{{col-begin}}

{{col-begin}}

{{col-break}}

{{col-break}}

* [http://mywikibiz.com/Propositional_calculus Propositional Calculus], [http://mywikibiz.com/ MyWikiBiz]

* [http://mywikibiz.com/Propositional_calculus Propositional Calculus], [http://mywikibiz.com/ MyWikiBiz]

* [http://planetmath.org/encyclopedia/PropositionalCalculus.html Propositional Calculus], [http://planetmath.org/ PlanetMath]

* [http://planetmath.org/encyclopedia/PropositionalCalculus.html Propositional Calculus], [http://planetmath.org/ PlanetMath]

* [http://www.getwiki.net/-Propositional_Calculus Propositional Calculus], [http://www.getwiki.net/ GetWiki]

* [http://www.getwiki.net/-Propositional_Calculus Propositional Calculus], [http://www.getwiki.net/ GetWiki]

* [http://www.textop.org/wiki/index.php?title=Propositional_calculus Propositional Calculus], [http://www.textop.org/wiki/ Textop Wiki]

* [http://www.textop.org/wiki/index.php?title=Propositional_calculus Propositional Calculus], [http://www.textop.org/wiki/ Textop Wiki]

* [http://en.wikipedia.org/w/index.php?title=Propositional_calculus&oldid=77110794 Propositional Calculus], [http://en.wikipedia.org/ Wikipedia]

* [http://en.wikipedia.org/w/index.php?title=Propositional_calculus&oldid=77110794 Propositional Calculus], [http://en.wikipedia.org/ Wikipedia]

{{col-end}}

{{col-end}}

[[Category:Charles Sanders Peirce]]

[[Category:Charles Sanders Peirce]]

[[Category:Computer Science]]

[[Category:Computer Science]]

[[Category:Formal Sciences]]

[[Category:Formal Sciences]]

[[Category:Formal Systems]]

[[Category:Formal Systems]]

[[Category:Linguistics]]

[[Category:Linguistics]]

[[Category:Logic]]

[[Category:Logic]]