Can you prove that proof exists?
>>17026757Yes. QEDQED
>>17026757Yes it's called a Zero-Knowledge Proof
>errrm agnostic skeptic here. errrm like we dont actually know if thingies are real or not!!!
>>17026757
>>17026798>Neoplatonist here. We actually don't know if relationships are real or not.
>>17026792Lmaoooo trueeeee
>>17026757>Can you prove that proof exists?Sometimes yes, this is called language/metalanguage distinction. See https://en.wikipedia.org/wiki/Reverse_mathematicshttps://plato.stanford.edu/entries/goedel-incompleteness/
Yes.
>>17026757Can you prove that their proof of dat proof is real?
>>17026757It depends on what you mean, but in lay speak, we prove they exist by construction. Formally, we will need to define a proof. This is conventionally done in proof theory through various proof systems (e.g. Natural Deduction, Sequent Calculi, Hilbert Calculi, etc).Once we have defined it, we can ask questions such as: "Does a proof of X exist". The statement "Does a proof exist" would be formalised as: "Does there exist a statement in a language that has a proof". This will be true since an axiom counts as a proof, since we generally assume a non-empty set of axioms. To give a concrete example we will use the following Hilbert Calculi for propositional logic:[eqn]\begin{align}(A1)\quad&p \to (q \to p)\\(A2)\quad&(p \to (q \to r)) \to ((p \to q) \to (p \to r))\\(A3)\quad&(\lnot p \to \lnot q) \to (q \to p)\end{align}[/eqn]To make this a usable proof system, we need the inference rule:[eqn]\begin{align*}(MP)\quad\text{If $p \to q$ and $p$, then $q$}\end{align*}[/eqn]Then we can prove [math](p \to q) \to (p \to p)[/math] as the following:1. [math]p \to (q \to p)[/math] by [math](A1)[/math]2. [math](p \to (q \to q)) \to ((p \to q) \to (p \to q))[/math] by [math](A2)[/math].3. Apply [math](MP)[/math] on (2) and (1) to get: [math]((p \to q) \to (p \to q))[/math]This provides a formal construction of a basic proof. For a more philosophical discussion, one could frame this question as the problem of universals (e.g. "Do numbers exist"). In that sense, one will have to deal with the same problems. However, proofs are closer to "writings" or "stories", which have less of a platonic ideal. I've tried to entertain the idea of the platonic ideal as much as I can in the previous description of formal proofs. Unfortunately, proving a proof exists tends be less of an interesting question.
