## State your conjecture...

*i.e.,*

## … or try one of these:

#### Propositional

- a \to \top
- a \to a
- a \to b \to a
- a \to a \and a
- a \and b \to b \and a
- a \to b \to b \and a
- (a \to b \to c) \to (a \to b) \to a \to c

#### Classically valid formulas (and their double negations)

- a \or (a \to \bot)

(not provable) - ((a \or (a \to \bot)) \to \bot) \to \bot
- ((a \to b) \to a) \to a

(not provable) - ((((a \to b) \to a) \to a) \to \bot) \to \bot

#### Instantiation

- \A [x, y] p (g x y) \to p (g x x)

(not provable) - p j \to \E [x] p x
- (\A [x] p x) \to p k
- (\E [x] p x \and (p x \to \bot)) \to \bot
- (\A [x] \E [y] r x y) \to (\E [w] \A [z] r z w)

(not provable) - (\E [w] \A [z] r z w) \to (\A [x] \E [y] r x y)
- (\A [x] p x) \to \E [y] p y

(not provable) - (\A [x] p x) \to \A [y] p y
- (\A [x] p x \to p (f x)) \to p j \to p (f (f j))

## Guide

### Concrete Syntax for Signatures

*Basic types*have the signature type`\type`

*Predicates*have types built with the type constructor`->`

with the target type`\o`

*Term constants*have types built with the infix type constructor`->`

`->`

is right-associative

### Concrete Syntax for Formulas

to get | write |
---|---|

\eq j k | `\eq j k` |

a \and b | `a \and b` or `a & b` |

\top | `\top` or `#t` |

a \or b | `a \or b` or `a | b` |

\bot | `\bot` or `#f` |

a \to b | `a \to b` or `a => b` |

\A [x] p x | `\A [x:i] p x` |

\E [x] p x | `\E [x:i] p x` |

[x] f x | `[x] f x` |

- Types can often be omitted after the variable in
`\A`

or`\E`

, i.e., they can be written`\A [x]`

or`\E [x]`

. When unambiguous, the types will be inferred. - The
connectives
`\and`

,`\or`

,`\to`

are right-associative and listed in the order of decreasing precedence. - Both
`\A [x:i]`

and`\E [x:i]`

behave like prefix connectives of the lowest precedence. - Due to an ambiguity in the LALR grammar, equality
`\eq`

cannot be written infix. This may be fixed with a hand-written LR parser in the future.