4 ms·
Formal verifiers don't verify axioms. You seem to envision formal verification only operating on some pre-agreed set of axioms, as if one can not use formal ve
by DoctorOetker 4y ago
Formal verifiers don't verify axioms.
You seem to envision formal verification only operating on some pre-agreed set of axioms, as if one can not use formal verification until the whole of humanity has agreed on them.
Unless one makes the overarching single theory a taboo there is in fact a single theory if you don't omit logical entailment operators as in modal accounts. See https://en.wikipedia.org/wiki/Logical_consequence#Modal_accounts https://en.wikipedia.org/wiki/Logical_consequence#Modal_acco...
Suppose Alice believes all humans are mortal:
Alice ⊢ X ∈ Human => Mortal(X)
And suppose Alice believes she is human herself:
Alice ⊢ Alice ∈ Human
Then she could conclude using a rule of inference (modus ponens) she believes in that she is mortal:
Alice ⊢ Mortal(Alice)
The same formal system can contain your beliefs, my beliefs, those of Newton and those of Einstein etc...
The turnstiles may be nested suppose Bob has expressed his beliefs, and Alice has found a statement resulting from Bob's beliefs, then she can express that he should then also believe that statement:
Alice ⊢ Bob ⊢ SomeStatementPerhapsEvenALogicalContradiction
All these turnstiles may be subscripted with a version or time indicator to model beliefs changing over time, such that when someone derives a contradiction from your believes you either drown in your own rules (principle of explosion) or reject at least one of your axioms that was used in the proof resulting in the contradiction (at the cost of losing the theorems that depended on that belief)...
Consider for example 2 encompassed theories, for simplicity chosen to be a plattitude of Newtonian physics and Special Relativistic physics:
Newton ⊢ SomeInstantaneousActionStatements
Einstein ⊢ ConstantSpeedOfLightInVacuumStatement
One and the same overarching theory can contain express all these theories, and we can exert pressures on one another to drop axioms, convince one another to promote a result to the status of an axiom (like Einstein proposed to bombard the deductions of Lorenz and others on the length contraction, field distortion and mass change in the back then seemingly very specific context of fast electrons in the theory of electromagnetism into fundamental mechanical postulates).
EDIT: the main reason people seem to believe in the strictly monotheistic applicability of formal verification is because they tend to only or mostly be exposed to mathematical statements where the boring repetitive turnstiles on the left are omitted for brevity
- simonh 4y agoI wasn't considering formal verification at all.
- DoctorOetker 4y agoI was in the original comment to which you had responded.