engleski

Formal Systems and Determinism

A formal system S can be conceived as a technical device, a Turing machine (TM, or a register machine) with the theorems of S as its output (Turing 1937, Gödel 1946, 1951, 1963, 1964). We formally describe the work of a TM in general by the use of causally adapted justification logic tools. Because of the halting problem, this formalization is dependent on an outer insight (oracle) into the work (halting/non-halting) of a TM. A TM works only piecemeal, on the ground of the current configuration and the instruction currently to be applied. We analyze some versions of "necessity" that exceed the concept of the mechanical determination by a formal proof because of the provable □¬□⊥ or its analogues (S4 translation of intuitionistic propositional calculus, the outline of justification logic in Gödel 1938). All versions include implicit or explicit quantification over (causal or proof) justifications. Gödel's concept of "absolute provability" is analyzed and related to Gödel's ontological proof.

formal proof, Turing machine, justification logic, abstract provability, causality

nije evidentirano