VazScep wrote:I should mention that truth-tables aren't in the formal semantics of propositional logic. They can't be, because in general, there can be infinitely many atoms, requiring infinitely large truth-tables.

Relatively speaking, a definition of the semantics for propositional logic requires little ingenuity, and as with everything in maths, there are many equivalent and perfectly sensible definitions. Off the top of my head:

A propositional alphabet is a (possibly infinite) set of symbols. Given an alphabet A, the propositional language L(A) consists of:

1) The elements of A.
2) ~p and p → q for any p and q in L(A).

An interpretation of L(A) is a function e from A to {0,1}, which is extended to a function e' from L(A) to {0,1} according to the rule that e'(~p) = 1 - e'(p) and e'(p → q) = 1 when p <= q and 0 otherwise.

We now talk stuff about the set of all functions e from A to {0,1} and their extensions e'.

What's your beef with this?

I have no beef with L(A). L(A) is fine all by itself. But where to next? Sets of sentences I don't think are part of L(A). Nor are arguments or validity or entailment. But it's all a choice I guess.

SpeedOfSound wrote:But you have indicated that you don't care about formal ideas in this regard.

Where do you get that idea? I just gave formal definitions of a propositional language and its interpretations. I care very much about doing this shit formally.

I have no beef with L(A). L(A) is fine all by itself. But where to next?

In any course on mathematical logic, you will go through the simple details of formally defining a proof and defining semantic entailment, and showing that these two coincide. It will involve talking about sets of propositions. In particular, following from the definitions I gave earlier, for any propositional alphabet A, and for any subset Γ of L(A), and for any p in L(A), I say that Γ ⊧ p holds if, for any interpretation e such that e(q) = 1 for any q in Γ, it is also the case that e(p) = 1.

Where do we need to talk about possible worlds or modalities?

VazScep wrote:

SpeedOfSound wrote:But you have indicated that you don't care about formal ideas in this regard.

Where do you get that idea? I just gave formal definitions of a propositional language and its interpretations. I care very much about doing this shit formally.

I have no beef with L(A). L(A) is fine all by itself. But where to next?

In any course on mathematical logic, you will go through the simple details of formally defining a proof and defining semantic entailment, and showing that these two coincide. It will involve talking about sets of propositions. In particular, following from the definitions I gave earlier, for any propositional alphabet A, and for any subset Γ of L(A), and for any p in L(A), I say that Γ ⊧ p holds if, for any interpretation e such that e(q) = 1 for any q in Γ, it is also the case that e(p) = 1.

Where do we need to talk about possible worlds or modalities?

Damn. How do make those symbols on this forum? Nothing I try from Da Google works. I can copy yours.

On the post. Thinking.

How many such interpretations are there to choose from?

VazScep wrote:...
An interpretation of L(A) is a function e from A to {0,1},
which is extended to a function e'
from L(A) to {0,1}
according to the rule that
e'(~p) = 1 - e'(p) and e'(p → q) = 1 when p <= q and 0 otherwise....

So I'm not getting this part.

This in particular "e'(~p) = 1 - e'(p) and e'(p → q) = 1"

is this: p <= q
reduction?

EDIT:
Now I see. You really meant:

which is extended to a function e'
from L(A) to {0,1}
according to the rule that
: e'(~p) = 1 - e'(p)
: e'(p → q) = 1 when p <= q and 0 otherwise....

where '-' and '<=' is arithmetic. That's surprising. Like playing monopoly and someone lays down a full house on Boardwalk.

How many such interpretations are there to choose from?

There are no restrictions on interpretations, so we're talking about all functions from the set of atoms to {0,1}. For n atoms, there are 2^n such functions. For infinitely many atoms, there are infinitely many functions.

The "-" and "<=" were arithmetic. Sorry if that wasn't clear. Interpreting → as less than or equal to is something I actively encourage. In intuitionistic logic, you have more than 2 truth-values, and there is a (partial) order on them. That means there is a relation "<=", but it's not the usual less-than or equal of arithmetic.

Here, you will still want to define p →q in terms of <=. We can say that when the truth value of p is less than or equal to the truth value of q, then p →q will have truth-value ⊤. This truth-value is called "top", and always denotes the maximum element, should it exist, of a partial order. By a clever pun, it can also be thought of as standing for big True, as in, as true as you can get.

Classical propositional logic is just a' special case where there are only two truth values, ⊤and ⊥ (top and bottom). There, you can just use arithmetic. Formally, sending ⊤ to 1 and ⊥ to 0 is a homomorphism.

If you're in Firefox, you can get the symbols by holding CTRL+SHIFT+U and then typing the unicode number.

VazScep wrote:

How many such interpretations are there to choose from?

There are no restrictions on interpretations, so we're talking about all functions from the set of atoms to {0,1}. For n atoms, there are 2^n such functions. For infinitely many atoms, there are infinitely many functions.

The "-" and "<=" were arithmetic. Sorry if that wasn't clear. Interpreting → as less than or equal to is something I actively encourage. In intuitionistic logic, you have more than 2 truth-values, and there is a (partial) order on them. That means there is a relation "<=", but it's not the usual less-than or equal of arithmetic.

Here, you will still want to define p →q in terms of <=. Here, we can say that when the truth value of p is less than or equal to the truth value of q, then p →q will have truth-value ⊤. This truth-value is called "top", and always denotes the maximum element, should it exist, of a partial order. By a clever pun, it can also be thought of as standing for big True, as in, as true as you can get.

Classical propositional logic is just a' special case where there are only two truth values, ⊤and ⊥ (top and bottom). There, you can just use arithmetic. Formally, sending ⊤ to 1 and ⊥ to 0 is a homomorphism.

If you're in Firefox, you can get the symbols by holding CTRL+SHIFT+U and then typing the unicode number.

Damn! I am in Firefox. Thanks.

Okay. Let me think it over. I should shut up for a few days now. Also I can't find the damned book that set me onto this path. Just had it the other day.

VazScep wrote:

SpeedOfSound wrote:But you have indicated that you don't care about formal ideas in this regard.

Where do you get that idea? I just gave formal definitions of a propositional language and its interpretations. I care very much about doing this shit formally.

I have no beef with L(A). L(A) is fine all by itself. But where to next?

In any course on mathematical logic, you will go through the simple details of formally defining a proof and defining semantic entailment, and showing that these two coincide. It will involve talking about sets of propositions. In particular, following from the definitions I gave earlier, for any propositional alphabet A, and for any subset Γ of L(A), and for any p in L(A), I say that Γ ⊧ p holds if, for any interpretation e such that e(q) = 1 for any q in Γ, it is also the case that e(p) = 1.

Where do we need to talk about possible worlds or modalities?

Are you just having a problem with calling the rows of a truth table or subsets of them 'possible worlds'?

SpeedOfSound wrote:Are you just having a problem with calling the rows of a truth table or subsets of them 'possible worlds'?

Are you serious? Calling rows of a truth table "possible worlds" doesn't show that propositional logic has anything to do with modal logic. It's just an incorrect and grossly misleading use of terms. Modal logic is about boxes, diamonds, and that accessibility relation which you gushed about earlier, confusing it with a directed graph.

You could call rows of a truth table "Prides and Prejudices", but it wouldn't make propositional logic a Jane Austen novel.

That would be a strong misreading of what I did say and what I am suggesting. Let's not pursue this again. Two different places.

In the meantime. What do you think of SML? I fell upon a course on my way to learning Haskell and got sidetracked. I like it a lot.

SpeedOfSound wrote:In the meantime. What do you think of SML? I fell upon a course on my way to learning Haskell and got sidetracked. I like it a lot.

I've written more SML than Haskell, but I always have more fun with Haskell. Which implementation of SML are you looking at?

VazScep wrote:

SpeedOfSound wrote:In the meantime. What do you think of SML? I fell upon a course on my way to learning Haskell and got sidetracked. I like it a lot.

I've written more SML than Haskell, but I always have more fun with Haskell. Which implementation of SML are you looking at?

Standard ML of New Jersey compiler (SML/NJ)

Haskell does look more fun. I'm thinking of doing a philosophy/logic project in SML though. Haven't decided yet. I have a few months before class starts.

SML was orginally purposed to write theorem provers, with algebraic datatypes purposed to define syntax recursively as I do above. In fact, all the definitions I gave correspond straightforwardly to recursive datatypes and recursive functions. If you're familiar with ML, the code is easier to understand than the maths, in my opinion.

Code: Select all

datatype 'a term = ATOM of 'a | NEG of 'a term | IMP of 'a term * 'a term

fun eval e (ATOM x)    = e x
  | eval e (NEG p)     = not (eval e p)
  | eval e (IMP (p,q)) = not (eval e p) orelse eval e q

Here, the alphabet A, which paramaterises the propositional language L(A), becomes a parametric type 'a with L(A) becoming 'a term in the ML.

That 'reads like math' bit has me as excited about this language as I was when I discovered c. Never since. Sure makes java seem like an old clunker and even c looks pale amateur.

I assume that C is mostly inspired by assembly languages and machine architectures, not mathematics.

ML is an extension of the typed lambda calculus, which was conceived of entirely independently of computers as a way to formalise mathematics more faithfully than predicate logic and set theory, by making function definition the most crucial concept. It arrived quite late on the scene after people had figured out how to implement these languages efficiently (you need a decent garbage collector for starters).

I've never looked at Fortran or MATLAB, but I guess they'll be very mathsy. The first of those has the fame of being one of the two oldest languages in existence that is still in use today (the other being Lisp), and I understand it takes inspiration from mathematics. In particular, I know that it follows static typing conventions of maths by insisting that "x", "y" and "z" should always denote reals while "m" and "n" should denote naturals. I can't see much to commend doing that, but then, I don't think we should take the notational conventions of mathematicians as gospel. I, for one, think that ML handles basic ideas such as multi-variate functions far more sanely than the average mathematician does. And like I said above, I think the ML description of propositional logic improves on the mathematical prose, and recursive data-types are a must in any statically typed language.

As is always the case when discussing programming languages, the less said about Java the better.

VazScep wrote:I assume that C is mostly inspired by assembly languages and machine architectures, not mathematics.

Yes. The great thing about c is that it is basically well written machine language. Nice direct translate.

VazScep wrote:SML was orginally purposed to write theorem provers, with algebraic datatypes purposed to define syntax recursively as I do above. In fact, all the definitions I gave correspond straightforwardly to recursive datatypes and recursive functions. If you're familiar with ML, the code is easier to understand than the maths, in my opinion.

Code: Select all

datatype 'a term = ATOM of 'a | NEG of 'a term | IMP of 'a term * 'a term

fun eval e (ATOM x)    = e x
  | eval e (NEG p)     = not (eval e p)
  | eval e (IMP (p,q)) = not (eval e p) orelse eval e q

Here, the alphabet A, which paramaterises the propositional language L(A), becomes a parametric type 'a with L(A) becoming 'a term in the ML.

Could you do me a favor?

Create a reasonably complex expression with that and evaluate it?

Code: Select all

val A = ATOM true;
val B = ATOM false;
val C = ATOM false;
val D = ATOM true;
val E = ATOM true;
     

See? This is one world. There are 32 possible worlds given that we have no constraints. Very simple.

Anyway. I figured out the usage. I'm on the second week of a course and somewhere around polymorphic types I became a little confused on possible syntax. It's a personal problem.

gak

Code: Select all

datatype 'a term = ATOM of 'a
  | NEG of 'a term
  | IMP of 'a term * 'a term

fun eval e (ATOM x)    = e x
  | eval e (NEG p)     = not (eval e p)
  | eval e (IMP (p,q)) = not (eval e p) orelse eval e q
 
       
val A = ATOM true;
val B = ATOM false;
val C = ATOM false;
val D = ATOM true;
val E = ATOM true;

val e1=NEG B;
val e2=IMP(C,A);


- eval e2;
stdIn:5.1-5.8 Error: operator and operand don't agree [tycon mismatch]
operator domain: 'Z -> bool
operand: bool term
in expression:
eval e2
-
Did I do some dumb shit here?

SpeedOfSound wrote:Create a reasonably complex expression with that and evaluate it?

First, a basic pretty-printer:

Code: Select all

fun pprint_term pprint_atom =
    let fun pp (ATOM x)    = pprint_atom x
          | pp (NEG p)     = "~" ^ pp p
          | pp (IMP (p,q)) = "(" ^ pp p ^ " => " ^ pp q ^ ")"
    in pp
    end

Here's the second axiom of Hilbert's propositional logic:

Code: Select all

val p = ATOM 0
val q = ATOM 1
val r = ATOM 2

val ax2 = IMP (IMP (p, IMP (q,r)), IMP (IMP (p,q), IMP (p,r)))

This pretty prints as:

Code: Select all

- pprint_term Int.toString ax2;
val it = "((0 => (1 => 2)) => ((0 => 1) => (0 => 2)))" : string

All evaluations of this expression yield true. Here's an example:

Code: Select all

- eval (fn n => Int.rem (n,2) = 0) ax2;
val it = true : bool