\ truth tables;

[dup #: 2 ^. _: !: 2 swap vs swap [` $.] map unit cons [set] each] 	`propositions 	def;
[dup "ABCDEFGHIJKLMNOPQRSTUVXYZ" lin &: @ ?:]				`letters	def; 
[dup letters propositions pop ck modality]				`prove		def;

[*: [&] iterate]							`tautology	def;
[~: tautology]								`contradiction	def;

[[[[tautology]		[pop `tautology]]
  [[contradiction]	[pop `contradiction]]
			[pop `contingent]] cond]			`modality	def;

[> ~:] 									`imp		def;
[[imp] [swap imp] cleave and popd] 					`iff 		def;

"P P not and" prove;
"P P not or" prove;
"P P Q imp and Q imp" prove;