Practice: Proof theory · The Lumenary

Proof theory

Warm-upHuman

Which rule of the one-sided calculus GS can introduce a formula that is not a subformula of its conclusion?

Choose one

Cut: from

\vdash \Gamma, A

and

\vdash \Gamma, A^\perp

infer

\vdash \Gamma

\wedge

: from

\vdash \Gamma, A

and

\vdash \Gamma, B

infer

\vdash \Gamma, A \wedge B

\vee

: from

\vdash \Gamma, A, B

infer

\vdash \Gamma, A \vee B

The axiom

\vdash \Gamma, p, \neg p

Proof theory

CoreHuman

In the lesson's proof of the Hauptsatz, the case $A = B \wedge C$ replaces one cut on $A$ by two cuts. What makes the induction go through?

Choose one

The new cut formulas

C

and

B

have fewer connectives than

A

.The new derivations are lower than the old ones.There are fewer cuts afterwards.The context

\Gamma

gets smaller.

Proof theory

CoreHuman

Which statement about cut elimination and proof length is correct?

Choose one

Eliminating cuts can make proofs vastly longer — non-elementarily so in first-order logic.Cut-free proofs are always shorter, since they contain no detours.Cut elimination preserves proof length up to a constant factor.Proof length is not meaningful because cut is admissible.

Proof theory

CoreHuman

Why is $\Rightarrow p \vee \neg p$ not derivable in LJ?

Choose one

A cut-free LJ proof of

\Rightarrow p \vee \neg p

would end with

\vee R

, so

\Rightarrow p

or

\Rightarrow \neg p

would be derivable — and neither is.Its truth table has a false row.LJ has no cut rule.LJ cannot express negation.

Proof theory

Warm-upHuman

The Goodstein sequence of $4$ starts $g_0 = 4$ (base 2) and $g_1 = 26$ (base 3), since $4 = 2^2 \mapsto 3^3 - 1 = 26$ . Compute $g_2$ .

Proof theory

StretchHuman

Which statement about $\mathsf{PA}$ and transfinite induction (for Gentzen's standard notation system) is correct?

Choose one

\mathsf{PA}

proves transfinite induction up to each

\alpha \lt \varepsilon_0

, but not up to

\varepsilon_0

.

\mathsf{PA}

proves transfinite induction up to

\varepsilon_0

, which is how it proves its own consistency.

\mathsf{PA}

proves transfinite induction only up to

\omega

, which is ordinary induction.Transfinite induction cannot be expressed in the language of arithmetic.

Proof theory

CoreFormal

The Lean proof of cut_admissible is cut_free_complete _ Γ rfl (soundness d). What does this tell you about the proof?

Choose one

It is the semantic route: a derivation with cuts is sound, and every valid sequent has a cut-free derivation.It is Gentzen's reduction: each cut is pushed upwards until it disappears.It assumes cut elimination as an axiom.It is trivial because Deriv false and Deriv true are the same predicate.

Proof theory

Warm-upFormal

In the Lean file, Deriv : Bool → List Fml → Prop. What does the Boolean argument control?

Choose one

Whether the cut rule may be used (true) or not (false).Whether the logic is classical or intuitionistic.Whether the sequent is valid.Whether weakening is allowed.

Proof theory

StretchComputational

Write bump(n, b), which writes $n$ in hereditary base $b$ (exponents in base $b$ too, recursively) and replaces every $b$ by $b + 1$ , and goodstein(n, steps), which returns the list $[g_0, g_1, \dots]$ of at most steps + 1 terms, stopping early at $0$ (start in base 2; $g_{k+1}$ = bump of $g_k$ in base $k + 2$ , minus 1).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.