# 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

### 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]))`.

## 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`.