[actuallyalys]

This back-and-forth makes me wonder, is it possible to write proofs about proofs? e.g., you cannot prove this result without logarithms or there must exist a proof that involves prime factors?

I suppose at least some proofs vaguely like that are possible because Gödel's incompleteness theorem is one, although I suspect that that same theorem puts some constraints on these "metaproofs."

[westurner]

Axiomatic system > Axiomatic method https://en.wikipedia.org/wiki/Axiomatic_system#Axiomatic_met...

Inference https://en.wikipedia.org/wiki/Inference ; inductive, deductive, abductive

Propositional calculus > Proofs in propositional calculus: https://en.wikipedia.org/wiki/Propositional_calculus

Quantum logic: https://en.wikipedia.org/wiki/Quantum_logic

https://twitter.com/westurner/status/1609495237738496000 :

> [ Is quantum logic the correct or a sufficient logic for propositional logic? ]

What are quantum "expectation values"; and how is that Axiomatic wave operator system different from standard propositional calculus?

[pdpi]

Well, Proof Theory is a branch of maths in its own right, and Category Theory also has a definite "meta-proof-y" feel to it.

[dvt]

> is it possible to write proofs about proofs

Yep, I took several metamathematics classes at UCLA! Mostly on proof theory, but also analyzing metamathematical results (like Godel's theorems, Henkin construction, and so on).