Discover Top Posts Tagged with #formal logic

Sis are you okay? You got so flustered you started denying the anticedent... You accidentally appealed to authority sis... you already know that makes your argument invalid... do you need a hug?

#formal logic #logic posting #i love formal logic #sis as a platonic replacement for bro #dont call me or my friends bro ill explode you with my mind powers

Proposal: Given a signature L equip the category of L-structures with some notion of 2-morphism such that the 1-equivalences become exactly the elementary L-embeddings?

#mathblr #model theory #category theory #logic #formal logic

∧ = mountain = difficult = strict condition = logical AND

∨ = valley = easy = weak condition = logical OR

(from AN #1261)

#mnemonic #formal logic #mathblr

classical logic vs intuitionistic logic

When I first heard about intuitionistic logic I was kind of confused. To quickly recap, classical logic is what we call 'normal logic' that you might have been taught in school. We have our AND, our OR, our NOTs, and so on. We also have some laws. For example, NOT (NOT (x)) is the same as x. When I learned about classical logic I thought it was obvious. What else could logic mean? But there are other logics, like intuitionistic logic. Intuitionistic logic *rejects* deducing x from NOT (NOT (x)). What does that even mean??? How does it make sense for NOT (NOT (x)) to be something other than x? What do you mean, "different logic"???? Thats nonsense!

The issue is that I had no idea about the difference between "syntax" and "semantics". In my introductory logic class I was taught there are two ways to prove logical statements - I can draw a big truth table, or I can use the laws of logical inference. The truth table is just me taking a logical formula and substituting in different truth values, and evaluating the operators. The laws of logical inference is applying a sequence of laws like "a AND b = b AND a" and "a AND a = a".

From a formal perspective, these are actually very different. The laws of logical inference are what are called "syntactic rules". That is, you don't need to assign a value to the terms you are operating on. You don't even need to know they represent truth values. You can just manipulate them formally. Using a big truth table is relying on what is called the "semantics" of the logic. That is, you need to remember that a term is either true or false, you need to remember the definitions of "AND" and "OR", and so on.

But there is something interesting about the syntactic rules.

There is nothing inherently "logic-ey" about them. There is nothing thats necessarily "TRUE" or "FALSE". There is a symbol for a tautology, a symbol for a contradiction, and so on, but the only reason we call them tautology or contradiction is because of their behaviour with AND and OR. The ideas of "TRUE" and "FALSE" that we are used to are just one *interpretation* of the rules of classical logic. That is, the laws of logical inference tell us how we can manipulate symbols on a page to 'deduce' things. They are a series of rules, or axioms if you wish, governing a set of values (which we may or may not choose to be TRUE and FALSE) and functions (which we may or may not choose to be NOT, AND, OR). The normal ideas of TRUE, FALSE, AND, NOT, and OR (called boolean logic) are meanings that we can substitute into the aforementioned manipulations that are consistent with them. (For whose who know what a model is, the syntactic rules are a theory, and boolean logic is a model of it.)

Isn't it interesting then that the things you can prove with the laws of logical inference are exactly the same as the things you can prove with a truth table, then? Maybe not. After all, we could just add deduction laws that are true (with respect to boolean logic) until we could prove everything we wanted to. For example, if we can't prove two things are equal that *should* be equal, just made the fact those two are equal a new law of logical inference. But what system do we get if we remove a "load bearing" law? For example, what if we no longer require that NOT (NOT (x)) = x? We would have a weaker system of axioms. We call this intuitionistic logic.

To be clear, you are still allowed to have a system for which that is true. Boolean logic is still a valid meaning to assign to intuitionistic logic, you just can't prove every statement of it. But are there any other interesting systems that satisfy this weaker set of laws? Can we call them "logic"?

Well I don't THINK of them as logic in the sense that they don't talk about truth. Instead the way to think about it is that classical logic is a set of laws that talk about truth, whereas intuitionistic logic is a set of laws that talk about constructability, or provability. For example, a statement is still either true or false. It is "obviously" always true that a statement is true or false. But it is not obviously true that a statement is either provable or disprovable. It is not necessarily true that you can either construct a proof or a counterexample.

Going back to "NOT NOT x = x". Lets say that "x" means "I can prove x", and "NOT x" means "I can disprove x". If I can disprove the fact that you can disprove x, that does not automatically mean that you can prove x. Maybe you can't prove or disprove it. Its still either true or false, we just can't prove it. This is a *different* interpretation of "NOT" and the term "x" that satisfies the rules of intuitionistic logic, but not classical logic. Note that if I can prove x, then I can definitely disprove the fact that you can disprove it. You just can't go the other way around.

So what is true (read: provable) in intuitionistic logic? You can't prove anything in intuitionistic logic that you can't prove in classical logic, because every valid law of deduction in intuitionistic logic is a valid law of classical logic. So we are able to prove strictly fewer things.

Why might we want to do this, then? In the realm of pure maths we often don't care about statements that are not decidable. Well that changes if we are working with a programming language. If I want to construct a function that returns me a value of some type, I want to see the actual value of the type. If I called a function and it just reassured me that there is an output value I'm looking for, I wouldn't be too happy about that. This links into type theory, computer proofs via types, and functional programming. It turns out there is a correspondance between computer programs (with types) and proofs in intuitionistic logic! Its called the "Curry Howard Correspondance". We think of every statement of logic corresponding to a type, and every proof of a statement corresponds to a value of that type. The details are below for those who are interested in computer types, and is pitched more for functional programming inclined people, and assumes some haskell to fully understand it, but is technically self contained?

An implication between two statements corresponds to a function between the two types. TRUE is any type that is inhabited, such as a "unit" type containing one element called (). FALSE is the type containing no values, called Void. NOT x is a function x -> Void. AND is the tuple type, and OR is the disjoint union (Either) type. For example if we have two types A and B, we can form a product type A x B, which has inhabitants of pairs (a,b) where a is type A and b is type B. Similarly we can form A | B which has inhabitants that are either Left a or Right b, where a is of type A and b is of type B.

The statement that A AND B is equivalent to B AND A is the fact that we can construct functions A x B -> B x A and B x A -> A x B, given by the swapping function (a, b) |-> (b,a). The statement that A AND TRUE is equivalent to A can be rethought of as the fact that there are functions between the types A and A x (), given by a |-> (a, ()) and (a, _) |-> a. The statement that A AND FALSE is equivalent to FALSE is the statement that A x Void has no elements.

The statement that NOT NOT x does not imply x is equivalent to the statement that there is no function with type ((x -> Void) -> Void) -> x. Imagine trying to construct such a function. You can't. You don't have any way to produce an x. Note that you can very easily create a function x -> ((x -> Void) -> Void). Thats just function application. Neat, huh?

Another interesting application of the difference between semantics and syntax in programming languages is Conal Elliott's "Compiling to Categories" paper, where he reinterprets the syntax of the programming language haskell to talk about different kinds of functions and objects.

#long post #functional programming #haskell #math #maths #formal logic #logic #mathematics