# ILogic¶

logic.spad line 2458 [edit on github]

parse result includes term returned and new index

- /\: (%, %) -> %
from MeetSemilattice

- =: (%, %) -> Boolean
returns

`true`

(boolean`true`

) if intuitionisticLogic values are the same. Translates from Intuitionistic Logic to Boolean Logic

- \/: (%, %) -> %
from JoinSemilattice

- _|_: %

- ~: % -> %
`~(x)`

returns the logical complement of`x`

. TODO not sure if complement should be included here? intuitionistic logic can have complement but has different axioms to complement in Boolean algebra. Equivalent capability can be provided by implication.

- atom?: % -> Boolean
returns

`true`

if this is an atom, that is a leaf node otherwise return`false`

if this is a compound term

- coerce: % -> OutputForm
from CoercibleTo OutputForm

- deductions: List % -> List %
assumes

`ln`

contains a list of factors which must be`true`

for the whole to be`true`

(such as the list produced by factor). From this deductions attempts to produce a list of other proposition that must also be`true`

by using modus ponens. This is used to determine the returned type when converting ILogic to types by using the Curry-Howard isomorphism.

- factor: % -> List %
splits

`n`

into a list of factors which must be`true`

for the whole to be`true`

. This assumes that the top level is already a set of factors separated by`/\`

otherwise the result will just be a list with one entry:`'n'`

. This is used when converting ILogic to types by using the Curry-Howard isomorphism.

- getChildren: % -> List %
returns child nodes if this is a compound term otherwise returns []

- implies: (%, %) -> %
`implies(a, b)`

returns the logical implication of ILogic a and`b`

. a is premise,`b`

is conclusion, result is`false`

(contradiction) if premise=true and conclusion=false does not mean there is a causal connection

- latex: % -> String
from SetCategory

- logicF: () -> %
`false`

(contradiction) is a logical constant.

- logicT: () -> %
`true`

is a logical constant.

- opType: % -> Symbol
if this is a compound op then opType returns the type of that op: “IMPLY”::Symbol =implies “AND”::Symbol=/“OR”::Symbol=

`\/`

“NOT”::Symbol=~ “OTHER”::Symbol=not compound op

- parseIL2: (String, NonNegativeInteger) -> Record(rft: %, pout: NonNegativeInteger)
Constructs intuitionistic logic terms from a string notation assumes format like this: <term2> :

`:=`

var | “(“<term>”)” <term> :`:=`

var | <term>/`\<`

term> | <term>`\/`

<term> | <term>-><term> | “(“<term>”)”

- parseIL: String -> %
Constructs intuitionistic logic terms from a string notation assumes format like this: <term> :

`:=`

var | <term>/`\<`

term> | <term>`\/`

<term> | <term>-><term> | “(“<term>”)”

- parseILTerm: (String, NonNegativeInteger) -> Record(rft: %, pout: NonNegativeInteger)
parseTerm is used by parseIL. It would rarely be called externally but it is here to allow it to call parseIL that is to allow circular calls

- proposition: String -> %
Constructs a proposition

- redux: % -> %
attempt to simplify theory apply recursively to subnodes normally this should not be necessary since logic values are interpreted when constructed

- T: %

- toString: % -> String
creates a string representation of this term and its sub-terms

- toStringUnwrapped: % -> String
similar to ‘toString’ but does not put outer compound terms in brackets

- value: % -> Symbol
returns: “T”::Symbol =

`T`

“F”::Symbol =`_|_`

“E”::Symbol = error “P”::Symbol = proposition “C”::Symbol = compound Constructs lambda term and bind any variables with the name provided