3 ms·

> There really is no difference between theory and practice. >But there is a big difference between theory and malpractice. If there was only one theory and i

by simonh 4y ago

> There really is no difference between theory and practice. >But there is a big difference between theory and malpractice. If there was only one theory and it had been verified absolutely, sure, but unfortunately that’s not the case. Not only are there many theories about many things, most of which are all mutually exclusive, but hardly any of them match with all the practical results anyway. That’s life.

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 ago
  I wasn't considering formal verification at all.
  - DoctorOetker 4y ago
    I was in the original comment to which you had responded.

by simonh 4y ago

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 ago
I wasn't considering formal verification at all.
- DoctorOetker 4y ago
  I was in the original comment to which you had responded.