✝️ Mark 1:1-3
The beginning of the good news of Jesus Christ.
As it is written in the prophet Isaiah,
“See, I am sending my messenger ahead of you,
who will prepare your way,
the voice of one crying out in the wilderness:
‘Prepare the way of the Lord;
make his paths straight,’ ”
So, I love logic and wanted to try world building so I picked FOL as the logic I wanted to use! You may ask how that is even possible and it goes something like [this](<#FOL example>), some problems with world building with FOL are that FOL is very limited and you cannot make things run, now I tried another "logic" called lambda calculus for my needs, it goes something like [this](<#lambda calc example>), but it can run but not assert! Now, FOL and lambda calc have other "problems" depending on how you look at them so I picked something called HOL! HOL is said to have more "problems" but I don't see it that way, I find the fact that HOL can state more than it can prove, amazing! I won't dive into the pros and cons of HOL, FOL, and lambda calculus but I will teach HOL because I find it fun! Let T1, T2, T3 be any term, let F1, F2, F3 be any formula, let V1, V2, V3 be any variable, let A1, A2, A3 be any type!
If you do not know what those concepts are, it is all good because I will teach them!
A term is an object like a number, a human, a red cube, etc! Now, a formula is a claim such as "the number is 225", "this cube is red", etc. Now, note that formulas can either be true or false. A variable is a placeholder and a type can be thought of as a label that says what kind of thing something is! Now, in HOL formulas ARE terms!
Now, every term has a type! The type for formulas is called o, short for omicron. The type for objects is called ι, short for iota! Now, say we have something like this: A1 → A2, the → symbol means a function that takes something of the type of A1 as input and outputs something of type A2! A function can be thought of as a little machine that you give input and it gives back output, for example say we have a little machine that takes a number and gives back the number plus 225! For example, you could give it 7 as input and the output would be 232! We can create functions like this and beyond: A1 → A2 → A3. Now, that example A1 → A2 → A3 would take something as input and output a function of type A2 → A3. Now, A1 → A2 → A3 is equal to A1 → (A2 → A3), it is not equal to (A1 → A2) → A3! A function that takes an ι as input and outputs an o is called a relation! For example: ι → o is a relation! Now, we have built in operators we can use and they are as follows!
T1 = T2 means T1 is equal to T2, = works on any type!
¬F1 means flip the truth value of F1!
F1 ∧ F2 means true if both F1 and F2 are true!
F1 ∨ F2 means true if F1, F2, or both are true!
F1 → F2 means false if F1 is true and F2 is false, else true!
F1 ↔ F2 means true if F1 and F2 have the same truth value!
∀V1 : A1 . F1 means true if F1 is true for every value of V1 of type A1!
∃V1 : A1 . F1 means true if F1 is true for at least one value of V1 of type A1!
T1 : A1 means the type of T1 is A1! Also it can introduce new stuff!
λV1 : A1 . T1 is different, it is a function that takes something of type A1 as input and outputs something of whatever the type of T1 is!
Now, note that → does two things, it can be used as a function type or as implication!
Now, λ is very powerful and can do stuff like below!
```
λx : ι . x
```
Well... that wasn't very powerful but this below is... still not!
```
λx : ι . λy : ι . λz : ι . x
```
That above one simplified just takes 3 arguments of type ι and outputs the first one, now to actually give input we would do this:
```
a: ι
b: ι
c: ι
(((λx : ι . λy : ι . λz : ι . x) a) b) c
=
((λy : ι . λz : ι . a) b) c
=
(λz : ι . a) c
=
a
```
Now, λ can do a lot more like this!
```
0: (ι → ι) → ι → ι
1: (ι → ι) → ι → ι
2: (ι → ι) → ι → ι
next : ((ι → ι) → ι → ι) → (ι → ι) → ι → ι
0 = (λx : ι → ι . λy : ι . y)
1 = (λx : ι → ι . λy : ι . x y)
2 = (λx : ι → ι . λy : ι . x (x y))
next = (λn : (ι → ι) → ι → ι . λx : ι → ι . λy : ι . x (n x y))
next 1
=
λx : ι → ι . λy : ι . x (1 x y)
=
λx : ι → ι . λy : ι . x ((λx : ι → ι . λy : ι . x y) x y)
=
λx : ι → ι . λy : ι . x ((λy : ι . x y) y)
=
λx : ι → ι . λy : ι . x (x y)
=
2
```
YAY! We have a NEXT function to get the number after the input number! Also the parentheses are used for grouping! Now, that is it for HOL besides the "problems" and stuff!
## [[#FOL example]]
```
∃rock∃paper∃scissors∃draw (
¬(rock = paper)
∧
¬(rock = scissors)
∧
¬(rock = draw)
∧
¬(paper = scissors)
∧
¬(paper = draw)
∧
¬(scissors = draw)
∧
∀option1∀option2 (
(
(option1 = rock
∨
option1 = paper
∨
option1 = scissors)
∧
(option2 = rock
∨
option2 = paper
∨
option2 = scissors)
)
→
∃winner (
(option1 = rock
∧
option2 = paper
∧
winner = paper)
∨
(option1 = rock
∧
option2 = scissors
∧
winner = rock)
∨
(option1 = paper
∧
option2 = rock
∧
winner = paper)
∨
(option1 = scissors
∧
option2 = rock
∧
winner = rock)
∨
(option1 = rock
∧
option2 = rock
∧
winner = draw)
∨
(option1 = paper
∧
option2 = scissors
∧
winner = scissors)
∨
(option1 = scissors
∧
option2 = paper
∧
winner = scissors)
∨
(option1 = paper
∧
option2 = paper
∧
winner = draw)
∨
(option1 = scissors
∧
option2 = scissors
∧
winner = draw)
)
)
)
```
## [[#lambda calc example]]
```
ROCK = λa.λb.λc.a
PAPER = λa.λb.λc.b
SCISSORS = λa.λb.λc.c
BEATS = λa.a PAPER SCISSORS ROCK
TRUE = λa.λb.a
FALSE = λa.λb.b
AND = λa.λb.a b FALSE
OR = λa.λb.a TRUE b
IS_ROCK = λa.a TRUE FALSE FALSE
IS_PAPER = λa.a FALSE TRUE FALSE
IS_SCISSORS = λa.a FALSE FALSE TRUE
EQUALS = λa.λb.OR (AND (IS_ROCK a) (IS_ROCK b)) (OR (AND (IS_PAPER a) (IS_PAPER b)) (AND (IS_SCISSORS a) (IS_SCISSORS b)))
DOES_FIRST_WIN = λa.λb.EQUALS a (BEATS b)
```