# Logstack

LogStack is a stack-based logic language created by User:Silver. Each item on the stack is a valid sentence of propositional logic, and all conditionals work by popping one and testing whether it can be proven using the rest of the stack as assumptions.

## Instructions

Instruction Effect
a-zA-Z push an atomic proposition corresponding to the letter
% push a tautology
& pop two propositions p and q, and push a compound proposition 'p and q'
| pop two propositions p and q, and push a compound proposition 'p or q'
! pop a proposition and push its negation
^ pop two propositions p and q and push 'p xor q'. This is syntactic sugar, under the hood all compound propositions are in terms of and, or and not
: pop two propositions p and q and push 'q implies p' (in that order, so "ab:" pushes a=>b)
= pop two propositions p and q and push 'p if and only if q' (biconditional)
/ swap the top two items on the stack
; duplicate the top item on the stack
@ rotate the stack - pop an proposition and place it on the bottom of the stack
~ pop a proposition and try to prove it using the rest of the stack. If it is provable, swap the top two items (not replacing the proposition popped for testing)
? pop a proposition and try to prove it. output the result ('yes' or 'no')
() loop - before each iteration, pop a proposition and try to prove it. If it's not provable, end the loop immediately
. halt the program
# output the state of the stack, mostly for debugging purposes

Any other character will be ignored.

## Computational Class

LogStack is Turing Complete, as proven by the following translation to 3-cell brainfuck:

Brainfuck LogStack
+ `%`
- `%/(ab)(%A(%B(C/ab)(Bab)\$/ab)(Aab)\$ab)\$`
> `(%@)%A(%B(C/ab)(Bab)\$/ab)(Aab)\$@`
< `(%@)%A(%B(C/ab)(Bab)\$/ab)(Aab)\$@(%@)%A(%B(C/ab)(Bab)\$/ab)(Aab)\$@`
[ `%(%/(`
] `%%ab)(%A(%B(C/ab)(Bab)\$/ab)(Aab)\$abc)\$)`

Which isn't as ugly as it looks (quite) once you realise that much of it is repeated `%A(%B(C/ab)(Bab)\$/ab)(Aab)\$`, which figures out which of A,B or C have just been popped and pushes the right one back.

## Use

As it turns out, the logic part isn't that much use. A subset of the language consisting only of three atomic propositions, %, /, \$, @ and () is Turing Complete, as shown above. However, there are a couple of useful things to remember:

• The difference between false and unprovable matters. `p?` on a stack that makes no mention of `p` outputs 'no'.
• The principle of explosion applies. If the stack implies a contradiction, all propositions are provable. This breaks the constructions below if it happens.
• the construction `%/( [if true] ab)( [if false] ab)\$` acts as an if-else statement
• the construction `*( [comment] )` allows comments

## Examples

### Truth Machine

Truthy input for this program consists of a starting stack containing a single 'p', falsy input is an empty starting stack.

```p        *(push (another?) 'p')
(        *(pop something, initially the 'p' we just pushed, and try to prove it. If it's not provable, skip past the matching ')')
pp?)    *(push two 'p's, then pop one of them and output whether or not it's provable - always yes. Then go back to the '(')
a?       *(push 'a' and output whether it's provable - always no, since it's not mentioned anywhere in the stack)```