Can computer science be used to "test" theories of logic?

Question

I feel like this might be a stupid question, like I think I've read at least one major text according to which, "Of course logics can be tested in a computer-science context, not necessarily in the sense of 'proving that a logic is true' but at least, rather, 'proving what the logic is useful for.'" Maybe I'm thinking of Douglas Hofstadter's quirky book.

Anyway, my question is at least whether we can evaluate the "physical realizability" of various logics in reference to computer science. I wouldn't expect such an evaluation to rule out logical pluralism too much, seeing as there are many programming languages, and then theoretical distinctions like "binary vs. quantum computation" are also important. But hardware still has to follow a relatively select set of principles to get going (use of specific materials in specific patterns, using specific electronic processes, etc.) and so I wonder if questions of combining logics or substructural logics could be answerable, at all, from a computer-science vantage. Like, if a logic has an untenable, if implicit, theory of (its own) syntax, then trying to embed/encode that logic in standard hardware will produce deviant or degenerate effects, maybe.

This might also be seen as having to do with the question of using the word "logic" as a mass noun. Plainly, we use the word "logic" as a count noun over inference systems that we intend to be "closed off" from each other, but in English, for example, we also say things like "x is more logical than b," which gets at a more "massive" reference style.

So assume (for the sake of argument) that perceptual consciousness is (effectively) continuous. Then go to a cardinality quantifier for ℝ (or whatever continuous set) and add on that we can intuitively plurally quantify over Continuum-many "objects" in continuous spacetime. If mass expressions can involve plural reference as directly as Boolos' quantifiers involve plural extension, yet if PQL goes to SOL (second-order logic), then could we say that there is a relationship between the continuous manifold of hardware possibilities in the physical world on the one hand, and the use of the word "logic" as a mass noun (in "informally rigorous" arguments from metalogic, i.e. in a second-order domain explicitly) on the other, such that we should expect to be able to interpret and resolve some problems in general theories of logic by invoking the results of applying this or that count-noun logic to a computer-science problem/hardware-implementation problem?

Is this just... trivial, even? My intuition is telling me that non-deductive methods of reasoning in mathematics are somehow relevant to the viability of my question, and to the triviality (or nontriviality) of possible answers.

Answer 1

Simply put, yes. And if computers are used from the vantage of cognitive scientists understanding human thought, it is called it experimental philosophy (SEP).

If you've followed some of my posts, you'll know I blather on about how logic is grounded in psychology, and the Fregean logicist program was a useful detour in the same way miasma theory lead to the death of countless pregnant women when Ignaz Semmelweis had irrefutable evidence washing hands after touching corpses and before delivering babies is a bad thing. Okay, hyperbolic a tad.

Brouwer inspired thinkers, and two of them were Heyting and Kolmogorov. In turn, they inspired Per Martin-Löf. His claim to fame is an intuitionist type theory (SEP). Think about that. Intuitionism rejects the notion that human minds are detached from deductivism, the classic fare of logical systems, and instead argues that logic systems are tools that harness psychological intuition; add to that a good type theory to avoid Russell's paradox, and you now have a radically different logical program from what Frege, Russell, and Tarski were working on. In fact, you might have the beginning of a formal theory pulling from multiple formal sciences that seeks to do mathematical reasoning like a human mind does. In his paper Truth of a Proposition, Evidence of a Judgement, Validity of a Proof, Martin-Löf goes on to reduce Heyting's, Kolmogorov's, and Gentzen's calculus to an isomorphism based on the premise that propositions are calls to the human mind to judge, not just truth conditions floating disembodied in a model-theoretic model. Incisively, he claims:

What is characteristic of this whole analysis, intuitionistic or verificationistic analysis, of the notions of proposition and truth is that the notion of proof of a proposition is conceptually prior (emphasis mine) to the notion of truth.

Whoa! He then goes on to trace this to Kant, talk about Bolzano, Brentano, and Husserl in much more detail. He then attempts to wrap up his excursion into historicity by arguing and drawing distinctions about realism and idealism, arguing essentially that appeals to correctness and the use of systems like Hoare's logic (not mentioned specifically), are grounded in the intuition of human judgement.

For computer scientists, any philosophical explication on correctness is extremely important because computer science, in the big picture, practices design (SEP), such as the design of languages, the design of specifications, and the design of computers. One of the primary questions in the process is, have I done it correctly? If you ever work as a software dev, you'll know that the constant baba yaga of coding is bugs. Bugs in the hardware, bugs in the EEPROM, bugs in the compiler, bugs in the code at compile-time and run-time, and bugs in other programmers' heads. Computer science myth literally tells of a moth stuck in a naval computer that Radm. Grace Hopper had to pluck from the circuits. (Also, see antipatterns for more information on an amusing canon of literature regarding the bugs generated by wetware.) Now, we are in a position to answer your question. To wit:

Can computer science be used to "test" theories of logic?

My dear sir, EVERY aspect of computer science is a test of theories of logic in one way or another. In intro discrete math courses, young computer scientists are taught that in 1854, George Boole in his book Laws of Thought essentially laid the golden egg for automatic computation by creating Boolean logic/algebra. The chapter that had that in my undergraduate education ended with using boolean algebra along side logic circuits check for correctness of design. So, computer scientists are obsessed with logics starting with the same fare that professional logicians are taught, and then diverging into their own domains. Algorithms, which are abstract maps to achieve goals are written in type-theoretic structures some of which, the functional sorts, are modeled on lambda calculus (which is equivalent to Turing's work). In fact, computer science in the modern sense began when Turing came to Princeton and along with other great mathematicians who invented computability theory (SEP), practiced mathematical logic. Kleene, Church, Turing? They were mathematical logicicans. I have a copy of Turing's thesis, and it's a logic. What makes computer science different from mathematical logic is not that mathematicians study logic and computer scientists study computers, no. It's that mathematicians run their mouths and produce fancy papers, but aren't constrained by the physical realities of having to build and operate computers that embody physical computation (SEP). (Platonic thinking is magical thinking when you have to build number systems from physical parts.) Traditionally, mathematicians play with abstract objects, and physicists build apparatuses to test physical objects; a computer scientist must master both domains. (Oversimplification, of course. Mathematical physics is arguably more math than physics, and applied mathematicians very much care about the correctness of their models; and the best and brightest thinkers in their field always have their nose in adjacent territory.)

I could spend all day waxing on about the relationship between computers and math, but my advice is you to read Colburn's Philosophy and Computer Science and then move on. Not my favorite, but it's a good start.

Is this just... trivial, even? My intuition is telling me that non-deductive methods of reasoning in mathematics are somehow relevant to the viability of my question, and to the triviality (or nontriviality) of possible answers

Oh, deduction, induction, and abduction are all absolutely part of the core of correctness, be it correctness of programming language semantics or microcode design on a VLSI, multi-core processor. Computer scientists are designers, and at all levels, correct design is imperative. Russell's type theory (computer's don't handle contradiction well) is the basis of all programming language design. For computer scientists, programming language primitives are signed and unsigned integers, booleans, floating point values, and strings, and those are types. And the imperative and declarative statements that use them often perform type checking both a compile-time and run-time. But programming language primitives are compositional objects built from data primitives in an operational code at the processor level. And what is the heart of a CPU? The ALU! The arithmetic-logic unit. If someone had a magic wand to turn the imaginary into something real, waving a wand over a logic system would produce a computer.

Induction, plays a role bridging the divide between the mathematical and hardware aspects on a pragmatic level. No matter how clever the wit and intentions of designers of all-things-computers, ultimately, there's no theoretical way to prove that physical implementations are correct except with inductive logic. And that inductive logic is physical experimentation. Build it, run it, and check the results. And AI folk figured out after ramming their head against the wall for a few decades that AI algorithms have to be constructed with probabilistic and defeasible logics (SEP). In fact, SEP has an entire entry dedicated to logic and artificial intelligence (SEP). Those are core inductive methods. Anyway, the details on AI stuff can be viewed looking at the encyclopedia of a textbook that is Russell and Norvig's (GB). You poke around there, and you'll see that all the chapters are just applications of three topics: statistics, algebra, and logic (with the exception of the robotics stuff).

Can computers be used to test logic? The answer is a resounding yes in more ways than I have textbooks on computers.

Answer 2

Computer Science, as a field, has made significant contributions to the study and understanding of logic and its applications. In fact, the study of logic and its application in computer science has a rich history, and the two fields have influenced each other in a number of ways.

In terms of evaluating the "physical realizability" of various logics, computer science provides a practical setting for testing and evaluating logical systems. For example, one can encode a given logic in a computer program and test its behavior in a variety of different scenarios. The success or failure of such tests can provide valuable insights into the strengths and weaknesses of different logics, and help us understand the conditions under which they are applicable.

Similarly, hardware constraints and design choices can also play a role in shaping the nature of logics that are used in computer science. For example, the principles underlying binary computation have a significant impact on the kinds of logics that are used to represent and manipulate data in a computer program.

In terms of the relationship between the physical world and theories of logic, it is indeed possible to argue that the possibilities and constraints of hardware implementation can play a role in shaping our understanding of logical systems. For example, certain logics may be more appropriate for certain hardware platforms than others, and this could help us evaluate and compare different logical systems.

while it may not be possible to "prove" the truth of a given logic using computer science, it is certainly possible to use computer science to test and evaluate different logical systems in terms of their applicability and feasibility in a practical setting. Additionally, the relationship between the physical world and theories of logic is an interesting and important area of study, and one that could have far-reaching implications for our understanding of logical systems and their applications.