Systems supported by Carnap
Carnap supports multiple "systems", i.e., languages with different symbols and syntax conventions, in the various types of exercises. For derivation exercises, a system implies a derivation system (set of rules, and derivation style). For truth table, translation, and counter-modeler exercises, the system implies a parser and a formula renderer, i.e., it implies which formulas are accepted as correct, how to parse them, and how to render formulas when they are displayed by Carnap.
All sentence letters, predicate symbols, constants, and function
symbols (if allowed) take subscripts (e.g., P_1
for P1).
Predicate and function symbols also take superscripts (e.g., P^1
for
P2) to indicate arity. The parser does not enforce the arity, i.e.,
the arity is always determined by the number of arguments actually
given.
The systems supported are:
- Bergmann, Moore & Nelson, The Logic Book
- Bonevac, Deduction
- Gallow, forall x: Pittsburgh
- Gamut, Logic, Language, and Meaning
- Goldfarb, Deductive Logic
- Hardegree, Symbolic Logic and Modal Logic
- Hausman, Kahane & Tidman, Logic and Philosophy
- Howard-Snyder, Howard-Snyder & Wasserman, The Power of Logic
- Hurley, Concise Introduction to Logic
- Ichikawa-Jenkins, forall x: UBC
- Johnson, forall x: Mississippi State
- Leach-Krouse, The Carnap Book
- Kalish & Montague, Logic
- Magnus, forall x
- Open Logic Project
- Thomas-Bolduc & Zach, forall x: Calgary
- Tomassi, Logic
Bergmann, Moore & Nelson, The Logic Book
Sentential logic
For the corresponding proof systems, see here.
- Selected with
system="..."
:LogicBookSD
LogicBookSDPlus
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
- Associative ∧, ∨: left
- Connectives:
Connective | Keyboard |
---|---|
⊃ | -> , => ,> |
& | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
~ | - , ~ , not |
Example:
`A /\ B /\ (C_1 -> (~R_2 \/ (S <-> T)))`{system="LogicBookSD"}
produces A /\ B /\ (C_1 -> (~R_2 \/ (S <-> T)))
.
Predicate logic
- Selected with
system="..."
:LogicBookPD
- Sentence letters:
A
...Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...v
- Function symbols: no
- Variables:
w
...z
- Atomic formulas: Fax
- Identity: no
- Quantifiers: (∀x), (∃x)
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
Example:
`(Ax)(Gabx -> (Ew)(Hxw /\ P))`{system="LogicBookPD"}
produces (Ax)(Gabx -> (Ew)(Hx /\ P))
Predicate logic with equality
- Selected with
system="..."
:LogicBookPDE
- Function symbols:
a
...t
- Variables:
w
...z
Connective | Keyboard |
---|---|
= | = |
Example:
`(Ax)(Gabx -> (Ew)(Hxw /\ P /\ ~f(x)=w))`{system="LogicBookPDE"}
produces (Ax)(Gabx -> (Ew)(Hxw /\ P /\ ~f(x)=w))
Bonevac, Deduction
Sentential logic
- Selected with
system="..."
:bonevacSL
- Sentence letters:
a
...z
- Brackets allowed
(
,)
- Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => , > |
& | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
Example:
`(a & b) & (c_1 -> (~r_2 \/ (s <-> t)))`{system="bonevacSL"}
produces (a /\ b) /\ (c_1 -> (~r_2 \/ (s <-> t)))
.
Quantificational logic
- Selected with
system="..."
:bonevacQL
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols:
a
...w
- Function symbols: none
- Variables:
x
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax(Gabx -> Ey(Hxy & Pa & ~x=v))`{system="bonevacQL"}
produces Ax(Gabx -> Ey(Hxy & Pa & ~x=v))
Gallow, forall x: Pittsburgh
For the corresponding proof systems, see here.
Sentential logic
- Selected with
system="..."
:gallowSL
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
,[
,]
- Associative ∧, ∨: left
Connective | Keyboard |
---|---|
→ | -> , => , > |
∧ | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
⊥ | !? , _|_ |
Example:
`A /\ B /\ (C_1 -> (~R_2 \/ [S <-> T]))`{system="gallowSL"}
produces A /\ B /\ (C_1 -> (~R_2 \/ [_|_ <-> T]))
.
First-order logic
- Selected with
system="..."
:gallowPL
- Sentence letters:
A
....Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...v
- Function symbols: none
- Variables:
w
...z
- Identity: no
- Atomic formulas: Fax
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
Example:
`Ax(Gabx -> Ew((Hxw /\ P) /\ Qs))`{system="gallowPL"}
produces Ax(Gabx -> Ew((Hxw /\ P) /\ Qs))
Gamut, Logic, Language, and Meaning
Propositional logic
- Selected with
system="..."
:gamutIPND
gamutPND
gamutPNDPlus
- Sentence letters:
a
...z
- Brackets allowed
(
,)
- Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => , > |
∧ | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
⊥ | !? , _|_ |
Example:
`(a /\ b) /\ (c_1 -> (~r_2 \/ (_|_ <-> t)))`{system="gamutIPND"}
produces (a /\ b) /\ (c_1 -> (~r_2 \/ (_|_ <-> t)))
.
Predicate logic
- Selected with
system="..."
:gamutND
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols:
a
...r
- Function symbols: none
- Variables:
s
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax(Gabx -> Ew(Hxw /\ (_|_ \/ ~x=w)))`{system="gamutND"}
produces Ax(Gabx -> Ew(Hxw /\ (_|_ \/ ~x=w)))
Goldfarb, Deductive Logic
Propositional logic
- Selected with
system="..."
:goldfarbPropND
- Sentence letters:
a
...z
- Brackets allowed
(
,)
- Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
⊃ | > , -> , ⊃ , → |
∙ | . , ∧ , ∙ |
∨ | \/ , | , or |
≡ | <-> , <=> , <> |
- | - , ~ , not |
⊥ | !? , _|_ |
Example:
`(a /\ b) /\ (c_1 -> (~r_2 \/ (_|_ <-> t)))`{system="goldfarbPropND"}
produces (a /\ b) /\ (c_1 -> (~r_2 \/ (_|_ <-> t)))
.
Predicate logic
- Selected with
system="..."
:goldfarbND
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols: none
- Function symbols: none
- Variables:
a
...z
- Atomic formulas: Fxy
- Identity: no
- Quantifiers: (∀x), (∃x)
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
Example:
`(Ax)(Gabx -> (Ew)(Hxw /\ P))`{system="goldfarbND"}
produces Ax(Gax -> Ew(Hxw /\ Pw))
Hardegree, Symbolic Logic
Sentential logic
- Selected with
system="..."
:hardegreeSL
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
- Associative ∧, ∨: left
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => ,> |
& | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
~ | - , ~ , not |
⨳ | !? , _|_ |
Example:
`A & G & (R_1 -> (~R_2 \/ (_|_ <-> T)))`{system="hardegreeSL"}
produces A & G & (R_1 -> (~R_2 \/ (_|_ <-> T)))
.
Predicate logic
- Selected with
system="..."
:hardegreePL
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols:
a
...s
- Function symbols: none
- Variables:
t
...z
- Atomic formulas: Fax
- Identity: no
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
Example:
`Ax(Gabx -> Ev(Hxe & Ov & _|_))`{system="hardegreePL"}
produces Ax(Gabx -> Ev(Hxe & Ov & _|_))
Hausman, Kahane & Tidman, Logic and Philosophy
Sentential logic
- Selected with
system="..."
:hausmanSL
- Sentence letters:
A
...Z
- Brackets allowed
[
,]
,(
,)
,{
,}
, (only in that order) - Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
⊃ | ⊃ , → ,> |
∙ | . , ∧ , ∙ |
∨ | \/ , | , or |
≡ | <-> , <=> , <> |
~ | - , ~ , not |
Example:
`[A . B] . [C_1 > (~R_2 \/ {S <> T})]`{system="hausmanSL"}
produces [A . B] . [C_1 > (~R_2 \/ {S <> T})]
.
Predicate logic
- Selected with
system="..."
:hausmanPL
- Sentence letters:
A
...Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...t
- Function symbols: no
- Variables:
u
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: (x), (∃x)
Quantifiers:
Connective | Keyboard |
---|---|
∃ | E |
= | = |
Example:
`(x)[Gabx > (Eu)(Hxu . {P \/ ~x=u})]`{system="hausmanPL"}
produces (x)[Gabx > (Eu)(Hxu . {P \/ ~x=u})]
Howard-Snyder, Howard-Snyder & Wasserman, The Power of Logic
Sentential logic
- Selected with
system="..."
:howardSnyderSL
- Sentence letters:
A
...Z
- With subscripts: ?
- Brackets allowed
(
,)
,[
,]
,{
,}
- Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => ,> |
∙ | . , ∧ , ∙ |
∨ | \/ , | , or |
↔︎ | <-> , <=> , <> |
~ | - , ~ , not |
Example:
`(A . B) . [C_1 -> (~R_2 \/ {S <-> T})]`{system="howardSnyderSL"}
produces (A . B) . [C_1 -> (~R_2 \/ {S <-> T})]
.
Predicate logic
- Selected with
system="..."
:howardSnyderPL
- Sentence letters:
A
...Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...u
- Function symbols: no
- Variables:
v
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: (x), (∃x)
Quantifiers:
Connective | Keyboard |
---|---|
∃ | E |
= | = |
Example:
`(x)[Gabx -> (Ev)(Hxv . (P \/ ~x=v))]`{system="howardSnyderPL"}
produces (x)[Gabx -> (Ev)(Hxv . (P \/ ~x=v))]
Hurley, Concise Introduction to Logic
Sentential logic
- Selected with
system="..."
:hurleySL
- Sentence letters:
A
...Z
- With subscripts: ?
- Brackets allowed
(
,)
,[
,]
,{
,}
- Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
⊃ | ⊃ , → ,> |
∙ | . , ∧ , ∙ |
∨ | \/ , | , or |
≡ | <-> , <=> , <> |
~ | - , ~ , not |
Example:
`(A . B) . [C_1 > (~R_2 \/ {S <-> T})]`{system="hurleySL"}
produces (A . B) . [C_1 > (~R_2 \/ {S <-> T})]
.
Predicate logic
- Selected with
system="..."
:hurleyPL
- Sentence letters:
A
...Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...w
- Function symbols: no
- Variables:
x
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: (x), (∃x)
Quantifiers:
Connective | Keyboard |
---|---|
∃ | E |
= | = |
Example:
`(x)[Gabx > (Ey)(Hxy . {P \/ ~x=y})]`{system="hurleyPL"}
produces (x)[Gabx > (Ey)(Hxy . {P \/ ~x=y})]
Ichikawa-Jenkins, forall x: UBC
Sentential logic
- Selected with
system="..."
:ichikawaJenkinsSL
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
,[
,]
- Associative ∧, ∨: yes
- Connectives:
Connective | Keyboard |
---|---|
⊃ | -> , => ,> |
& | /\ , & , and |
∨ | \/ , | , or |
≡ | <-> , <=> |
¬ | - , ~ , not |
Example:
`A /\ B /\ (C_1 -> (~R_2 \/ [S <-> T]))`{system="ichikawaJenkinsSL"}
produces A /\ B /\ (C_1 -> (~R_2 \/ [S <-> T]))
.
Quantificational logic
- Selected with
system="..."
:ichikawaJenkinsQL
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols:
a
...w
- Function symbols: none
- Variables:
x
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax(Gabx -> Ey(Hxy /\ Pa /\ ~x=y))`{system="ichikawaJenkinsQL"}
produces Ax(Gabx -> Ey(Hxy /\ (Pa /\ ~x=y)))
Johnson, forall x: Mississippi State
For the corresponding proof systems, see here.
- Selected with
system="..."
:johnsonSL
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
,[
,]
- Associative ∧, ∨: yes
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => ,> |
& | /\ , & , and |
∨ | v , \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
Example:
`A & B & (C_1 -> (~R_2 \/ [S <-> T]))`{system="johnsonSL"}
produces A & B & (C_1 -> (~R_2 \/ [S <-> T]))
.
Leach-Krouse, The Carnap Book
Kalish & Montague, Logic
For the corresponding proof systems, see here.
Propositional logic
- Selected with
system="..."
:prop
,montagueSC
- Sentence letters:
P
...W
- Brackets allowed
(
,)
- Associative ∧, ∨: left
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => ,> |
∧ | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
Example:
`P /\ Q /\ (R_1 -> (~R_2 \/ (S <-> T)))`{system="prop"}
produces P /\ Q /\ (R_1 -> (~R_2 \/ (S <-> T)))
.
First-order logic
- Selected with
system="..."
:firstOrder
,montagueQC
- Sentence letters:
P
...W
- Predicate symbols:
F
...O
- Constant symbols:
a
...e
- Function symbols:
f
...h
- Variables:
v
...z
- Atomic formulas: F(a,x)
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax(G(a,f(b),x) -> Ev(H(x,v) /\ P /\ ~(x=v)))`{system="firstOrder"}
produces Ax(G(a,f(b),x) -> Ev(H(x,v) /\ P /\ ~(x=v)))
Monadic second-order logic
- Selected with
system="..."
:secondOrder
- Second-order variables:
X
...Z
Symbols:
Connective | Keyboard |
---|---|
λ | \ |
Example:
Example:
`AX(\x[Ey(F(y) /\ X(x))](a))`{system="secondOrder"}
produces AX(\x[Ey(F(y) /\ X(x))](a))
Polyadic second-order logic
- Selected with
system="..."
:polyadicSecondOrder
- Second-order variables:
Xn
...Zn
- Arity: given by n
Example:
`AX2(\x[Ay(F(y) -> X2(x,y))](a))`{system="polyadicSecondOrder"}
produces AX2(\x[Ay(F(y) -> X2(x,y))](a))
Magnus, forall x
Sentential logic
- Selected with
system="..."
:magnusSL
magnusSLPlus
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
,[
,]
- Associative ∧, ∨: yes
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => ,> |
& | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
Example:
`A & B & (C_1 -> (~R_2 \/ [S <-> T]))`{system="magnusSL"}
produces A & B & (C_1 -> (~R_2 \/ [S <-> T]))
.
Quantificational logic
- Selected with
system="..."
:magnusQL
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols:
a
...w
- Function symbols: none
- Variables:
x
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax(Gabx -> Ey(Hxy & Pa & ~x=v))`{system="magnusQL"}
produces Ax(Gabx -> Ey(Hxy & Pa & ~x=v))
Open Logic Project
Plain propositional and first-order logic uses the same syntax as the
TFL and FOL systems of forall x: Calgary, 2019+ version (see below.
The parser for openLogicNK
and openLogicLK
is synonymous with
thomasBolducAndZachTFL2019
; and openLogicFOLNK
and
openLogicFOLLK
with thomasBolducAndZachFOL2019
.
Two OLP proof systems are supported: sequent calculus and natural deduction.
In addition, there are special systems supporting the language of arithmetic and the language of set theory.
Arithmetic
- Selected with
system="..."
:openLogicArithNK
- Predicate symbols:
<
(two-place, infix) - Constant symbols:
a
...r
,0
- Function symbols:
'
(one-place, postfix),+
,*
(two-place, infix) - Variables:
s
...z
- Identity:
=
,≠
Symbol | Keyboard |
---|---|
× | * |
≠ | != |
Example:
`AxAy x * y' = (x * y) + y /\ Ax(0!=x -> 0<x)`{system="openLogicArithNK"}
produces AxAy x * y' = (x * y) + y /\ Ax(0!=x -> 0<x)
Extended Arithmetic
- Selected with
system="..."
:openLogicExArithNK
- Predicate symbols: strings beginning with uppercase letter,
<
(two-place, infix) - Constant symbols: strings beginning with lowercase letter,
0
- Function symbols: strings beginning with lowercase letter,
'
(one-place, postfix),+
,*
(two-place, infix) - Variables:
s
...z
- Identity:
=
,≠
Symbol | Keyboard |
---|---|
× | * |
≠ | != |
Example:
`Q_1(0,0') /\ Ax(0<x -> Sq_a(0,x))`{system="openLogicExArithNK"}
produces Q_1(0,0') /\ Ax(0<x -> Sq_a(0,x))
Set theory
- Selected with
system="..."
:openLogicSTNK
- Predicate symbols:
∈
(two-place, infix) - Constant symbols:
a
...r
- Variables:
s
...z
- Identity:
=
,≠
The system openLogicExSTNK
is like the above but adds arbitrary
string predicates and function symbols:
- Selected with
system="..."
:openLogicExESTNK
- Predicate symbols: strings beginning with uppercase letter
- Constant symbols: strings beginning with lowercase letter
- Function symbols: strings beginning with lowercase letter
Symbol | Keyboard |
---|---|
∈ | << , <e |
≠ | != |
Example:
`Ex(Ay ~y<<x /\ Az(z!=x -> Eu u<<z))`{system="openLogicSTNK"}
produces Ex(Ay ~y<<x /\ Az(z!=x -> Eu u<<z))
Extended set theory
- Selected with
system="..."
:openLogicESTNK
,openLogicExESTNK
- Predicate symbols:
∈
,⊆
(two-place, infix) - Constant symbols:
∅
,a
...r
- Function symbols:
∪
,∩
,/
,Pow
(two-place, infix) - Variables:
s
...z
- Identity:
=
,≠
The system openLogicExESTNK
is like the above but adds arbitrary
string predicates and function symbols:
- Selected with
system="..."
:openLogicExESTNK
- Predicate symbols: strings beginning with uppercase letter
- Constant symbols: strings beginning with lowercase letter
- Function symbols: strings beginning with lowercase letter
Symbol | Keyboard |
---|---|
∅ | {} , empty |
∈ | << , <e , in |
⊆ | <( , <s , within , sub |
∪ | U , cup |
∩ | I , cap |
/ | \ |
Pow | P |
≠ | != |
Example:
`Ex(Ay ~y<<x /\ Az(z!={} -> Eu u <( P(z)))`{system="openLogicESTNK"}
produces Ex(Ay ~y<<x /\ Az(z!={} -> Eu u <( P(z)))
Thomas-Bolduc & Zach, forall x: Calgary
For the corresponding proof systems, see here.
Fall 2019 and after
The 2019
systems refer to the syntax used in forall x: Carnap,
Fall 2019 and after. The TFL system allows leaving out extra
parentheses in conjunctions and disjunctions of more than 2 sentences.
The pre-2019 systems do not, so can be used if stricter parenthesis
rules are desired.
The major change is in the syntax of the FOL systems, which wrap
arguments in parentheses. This allows support of function symbols and
terms. The FOL2019
system also allows entering negated identities as
x != y
. This is not done in forall x: Calgary, but is the
convention in the Open Logic Project.
Truth-functional logic
- Selected with
system="..."
:thomasBolducAndZachTFL2019
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
,[
,]
- Associative ∧, ∨: left
Connective | Keyboard |
---|---|
→ | -> , => , > |
∧ | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
⊥ | !? , _|_ |
Example:
`A /\ B /\ (C_1 -> (~R_2 \/ [S <-> T]))`{system="thomasBolducAndZachTFL2019"}
produces A /\ B /\ (C_1 -> (~R_2 \/ [_|_ <-> T]))
.
First-order logic
- Selected with
system="..."
:thomasBolducAndZachFOL2019
,thomasBolducAndZachFOLPlus2019
- Sentence letters:
A
....Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...r
- Function symbols:
a
...t
- Variables:
s
...z
- Atomic formulas: F(a,x)
- Identity:
=
,≠
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
≠ | != |
Example:
`Ax(G(a,f(b),x) -> Es(H(x,s) /\ P /\ x!=s))`{system="thomasBolducAndZachFOL2019"}
produces Ax(G(a,f(b),x) -> Es(H(x,s) /\ P /\ x!=s))
pre-Fall 2019
These syntax conventions were in force before the Fall 2019 edition of forall x: Calgary. They are still useful: (a) They coincide with the syntax conventions of Tim Button's forall x: Cambridge and the text by Sean Ebbels-Duggan. (b) The TFL system requires all parentheses be included and displays with all parentheses. So it can be used in exercises that require TFL sentences be entered or displayed without bracketing conventions.
Truth-functional logic
- Selected with
system="..."
:thomasBolducAndZachTFL
,ebelsDugganTFL
- Sentence letters:
A
...Z
- Brackets allowed
(
,)
,[
,]
- Associative ∧, ∨: no
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => , > |
∧ | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
¬ | - , ~ , not |
⊥ | !? , _|_ |
Example:
`(A /\ B) /\ (C_1 -> (~R_2 \/ [_|_ <-> T]))`{system="thomasBolducAndZachTFL"}
produces (A /\ B) /\ (C_1 -> (~R_2 \/ [_|_ <-> T]))
.
Example:
`(A /\ B) /\ (C_1 -> (~R_2 \/ [_|_ <-> T]))`{system="ebelsDugganTFL"}
produces (A /\ B) /\ (C_1 -> (~R_2 \/ [_|_ <-> T]))
.
First-order logic
- Selected with
system="..."
:thomasBolducAndZachFOL
- Sentence letters:
A
....Z
- Predicate symbols:
A
...Z
- Constant symbols:
a
...r
- Function symbols: none
- Variables:
s
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax(Gabx -> Es(Hxs /\ P /\ ~x=s))`{system="thomasBolducAndZachFOL"}
produces Ax(Gabx -> Es(Hxs /\ (P \/ ~x=s)))
Tomassi, Logic
Propositional logic
- Selected with
system="..."
:tomassiPL
- Sentence letters:
P
...W
- Brackets allowed
(
,)
- Associative ∧, ∨: left
- Connectives:
Connective | Keyboard |
---|---|
→ | -> , => ,> |
& | /\ , & , and |
∨ | \/ , | , or |
↔︎ | <-> , <=> |
~ | - , ~ , not |
Example:
`P /\ Q /\ (R_1 -> (~R_2 \/ (S <-> T)))`{system="tomassiPL"}
produces P /\ Q /\ (R_1 -> (~R_2 \/ (S <-> T)))
.
Predicate logic
- Selected with
system="..."
:tomassiQL
- Sentence letters: none
- Predicate symbols:
A
...Z
- Constant symbols:
a
...t
- Function symbols: none
- Variables:
u
...z
- Atomic formulas: Fax
- Identity:
=
- Quantifiers: ∀x, ∃x
Quantifiers:
Connective | Keyboard |
---|---|
∀ | A |
∃ | E |
= | = |
Example:
`Ax[Gabx -> Ev(Hxv /\ Pr /\ ~(x=v))]`{system="tomassiQL"}
produces Ax[Gabx -> Ev(Hxv /\ Pr /\ ~(x=v))]
Todo:
The available set theory systems are: elementarySetTheory
and
separativeSetTheory
. The available propositional modal logic systems
are: hardegreeL
hardegreeK
hardegreeT
hardegreeB
hardegreeD
hardegree4
and hardegree5
. The available predicate modal logic
system is hardegreeMPL
, and the available "world theory" system is
hardegreeWTL
.