# ILogicΒΆ

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
- _|_: %
- from BoundedJoinSemilattice

- ~: % -> %
`~(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.- ~=: (%, %) -> Boolean
- from BasicType

- 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 []
- hash: % -> SingleInteger
- from SetCategory
- hashUpdate!: (HashState, %) -> HashState
- from SetCategory

- 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: %
- from BoundedMeetSemilattice

- 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