Tautology and Contradiction

 We will see here how we can construct truth tables for finding tautology and contradiction. We use here static functions (Called with @ before name) and subs, which are part of same "parent" module, where parent means here a module/function which contains source of child functions/modules. Static functions and sub aren't owner of a scope, but any local variable removed at the exit/return from the call. One reason for anyone to use a static part of code, is the compactness of code.

Modules and normal functions have own scope, and we can call anything we define there, but not something which an inner module define. To use something defined before the call of a module we have to pass it as parameter, or to have it as global. Any local definition hide any global with same name, but if we call an inner module the global one aren't hidden until we define a same name definition.

Identifier True and False are double type values -1 and 0, so here we want to be Boolean. One way to do that is by defining constants. The values after boolean= can be zero or non zero, or False and True (which are the standard True and False, not the new defined).

Especially for global constants we can use a statement like const True, False to check if these constants exist as user's constants (not the predefined True and False). If we place a const bool True =@True which make a local constant then we hide the global one, and this isn't bad, because we have the same result here, but if we need to use a constant value say 1234 which defined globally (until the module which define it exit execution), with a name ABC, a statement ABC=100 make a local variable which hide the global constant, and change the ABC from constant to a variable. So if we use Const ABC without providing a value, interpreter check if there is a global constant ABC and if found one make a reference ABC as local to the global constant, so now a ABC=100 will raise error, because ABC exist as  local constant. If nothing found, at Const ABC statement, interpreter raise error, for missing constant.

In M2000 not all inner modules defined on same source as the parent. We can load modules from disk using Load statement on any module or function.  Interpreter use a cashed list of functions depending on loading modules, and we can exclude cash list using properly the load function.

Module CanonicalForms2 {
	Font "Verdana"
	linespace 0
	form 60
	global const True as boolean=True, False as boolean=False
	module tautology {
		const True, False
		print part "  tautology based on truth table: P ∨ ¬P"
		print Under $(7),"P", "¬P", "P ∨ ¬P"
		print under
		P = (True, False)
		Q = (True, False)
		eP = Each(P)
		boolean acc=true
		While eP
			acc = acc and @P() or not @P()
			print @P(), not @P(), @P() or not @P() 
		end While
		tautology(acc)
		print
		print part "  tautology based on truth table: P → (Q → P)"
		print Under $(7),"Q", "P", "Q → P", "P → (Q → P)"
		print Under
		acc = True
		eP = Each(P)
		While eP
			eQ=Each(Q)
			While eQ
				acc = acc and @implication(@P(), @implication(@Q(),@P()))
				print @Q(), @P(),  @implication(@Q(),@P()), @implication(@P(), @implication(@Q(),@P()))
			end While
		end While	
		tautology(acc)
		print	
	}
	module contradiction {
		const True, False
		print part "  contradiction based on truth table: P ∧ ¬P"
		print Under $(7),"P", "¬P", "P ∧ ¬P"
		print under
		P = (True, False)
		Q = (True, False)
		eP = Each(P)
		boolean acc=false
		While eP
			acc = acc or @P() and not @P()
			print @P(), not @P(), @P() and not @P() 
		end While
		contradiction(acc)
		print
		print
		print part " contradiction based on truth table: ¬(P ∨ ¬(P ∧ Q))"
		print Under $(7),"P", "Q", "P ∧ Q","¬(P ∧ Q)", "P ∨ ¬(P ∧ Q)","¬(P ∨ ¬(P ∧ Q))"
		print Under
		acc = false
		eP = Each(P)
		While eP
			eQ=Each(Q)
			While eQ
				acc = acc and not (@P() or not (@P() and @Q()))
				print @P(), @Q(), @P() and @Q(), not (@P() and @Q()),
				print @P() or not (@P() and @Q()), not (@P() or not (@P() and @Q()))
			end While
		end While	
		contradiction(acc)
	}
	module check_for_contradiction_or_tautology {
		const True, False
		print
		print part "  check for contradiction and tautology: (P → Q)→ P"
		print Under $(7),"P", "Q", "P → Q", "(P → Q)→ P"
		print under
		P = (True, False)
		Q = (True, False)
		eP = Each(P)
		boolean acc1=true, acc2=false, res
		While eP
			eQ=Each(Q)
			While eQ
				res = @implication(@implication(@P(),@Q()),@P())
				acc1 = acc1 and res
				acc2 = acc2 or res
				print @P(), @Q(), @implication(@P(),@Q()), res
			end While
		end While
		tautology(acc1)
		contradiction(acc2)
	}
	tautology
	contradiction
	check_for_contradiction_or_tautology
	push key$
	drop
	// inner modules can found static functions on the parent, which are in the same code
	// but variables scope isn't extend to parent.
	// So eP and eQ must defined prior to call  these functions
	function implication(P as boolean, Q as boolean)
		// canonical form
		=Not P Or Q
	end function
	function P()
		=array(eP)
	end function
	function Q()
		=array(eQ)
	end function
	sub tautology(acc as boolean)
		if acc then
			print  "we have tautology, all True"
		else
			print  "we haven't tautology, not all True"
		end if
	end sub
	sub contradiction(acc as boolean)
		if not acc then
			print  "we have contradiction, all False"
		else
			print  "we haven't contradiction, not all False"
		end if
	end sub
}
CanonicalForms2