<p>Is logic in computation of computation constructivist?</p>
<p>I think so, because dynamic languages ​​are comparable to constructivist set theory (try a demonstration of the axiom of choice in computing: it is inconstructible (there is a solution but it is not necessarily the axiom of original choice, which according to the theorem from Diaconescu, it's unconstructible)), you can't invoke objects out of thin air in computing... even the real ones are constructive. It may seem that the binary model introduces a binary logic into computation, where the LEM holds, but this only serves for propositions reducible to logic gates (i.e., trivial); when it is not, it is up to the CISC processor to resolve these complex instructions by tri-valued logic (in newer versions of binary hardware, this is not even necessary, as there is a third value between 0 and 1 that indicates a &quot;gap&quot;), and even RISC hardware implement complex interface underneath but present RISC interface. I think your confusion is the question of computability theory (as opposed to recursion theory), which is a classical (Platonist) mathematical theory, which imports the concept of computability (just as it imports concepts of intensionality and metamathematics), but within of computation itself, such concepts are not introduced from outside, but are the computation process itself, the semantics itself. And natural deduction, in vdd initially there was no LEM (because Gentzen wanted to build a logic exactly the way we think), and as at the time this would be seen with bad eyes, he corrected it by adding LEM as an axiom. In constructivism there is not even an axiom.</p>

<cc.complexity-theory><linear-logic>
Is logic in computation of computation constructivist?
Lambert macuse
# Is logic in computation of computation constructivist?

(Asked by: username_0 on 2022-08-16)

Is logic in computation of computation constructivist?

I think so, because dynamic languages ​​are comparable to constructivist set theory (try a demonstration of the axiom of choice in computing: it is inconstructible (there is a solution but it is not necessarily the axiom of original choice, which according to the theorem from Diaconescu, it's unconstructible)), you can't invoke objects out of thin air in computing... even the real ones are constructive. It may seem that the binary model introduces a binary logic into computation, where the LEM holds, but this only serves for propositions reducible to logic gates (i.e., trivial); when it is not, it is up to the CISC processor to resolve these complex instructions by tri-valued logic (in newer versions of binary hardware, this is not even necessary, as there is a third value between 0 and 1 that indicates a "gap"), and even RISC hardware implement complex interface underneath but present RISC interface. I think your confusion is the question of computability theory (as opposed to recursion theory), which is a classical (Platonist) mathematical theory, which imports the concept of computability (just as it imports concepts of intensionality and metamathematics), but within of computation itself, such concepts are not introduced from outside, but are the computation process itself, the semantics itself. And natural deduction, in vdd initially there was no LEM (because Gentzen wanted to build a logic exactly the way we think), and as at the time this would be seen with bad eyes, he corrected it by adding LEM as an axiom. In constructivism there is not even an axiom.

**Tags:** cc.complexity-theory, linear-logic

---

## 0 answers

