N-place implicational tautologies

Diving into Mathematical Logic brought me across Peirce’s Law, which uses the logical implication ⇒ operator only and is always True irrespective of what its two inputs (say) P and Q are:

((P ⇒ Q) ⇒ P) ⇒ P

Tower of N-place implicational tautologies

This got me thinking about the possibility of logical formulae that only use the logical implication ⇒ operator and are always True for any number of inputs.

A Hierarchy of Laws

I investigated this with some Python code and it turns out that there is a hierarchy of Laws:

Number of Variables – ArityVariablesNumber of Shortest TautologiesShortest Tautologies
(Unique up to variable renaming)
Comments
01True
1P1P ⇒ P
2P, Q2P ⇒ (Q ⇒ P)
P ⇒ (Q ⇒ Q)
Peirce’s Law is just one of sixteen two-variable tautologies with three ⇒ operators:
P ⇒ ((P ⇒ Q) ⇒ P)
P ⇒ (P ⇒ (Q ⇒ P))
(P ⇒ Q) ⇒ (P ⇒ Q)
P ⇒ (Q ⇒ (P ⇒ Q))
(P ⇒ Q) ⇒ (Q ⇒ Q)
P ⇒ (Q ⇒ (Q ⇒ Q))
((P ⇒ Q) ⇒ P) ⇒ P
P ⇒ ((Q ⇒ P) ⇒ P)
(P ⇒ Q) ⇒ (P ⇒ P)
P ⇒ (Q ⇒ (P ⇒ P))
P ⇒ ((Q ⇒ Q) ⇒ P)
P ⇒ (Q ⇒ (Q ⇒ P))
((P ⇒ P) ⇒ Q) ⇒ Q
P ⇒ ((P ⇒ Q) ⇒ Q)
(P ⇒ P) ⇒ (Q ⇒ Q)
P ⇒ (P ⇒ (Q ⇒ Q))
3P, Q, R5(P ⇒ Q) ⇒ (R ⇒ R)
P ⇒ (Q ⇒ (R ⇒ R))
P ⇒ (Q ⇒ (R ⇒ Q))
P ⇒ ((Q ⇒ R) ⇒ P)
P ⇒ (Q ⇒ (R ⇒ P))
4P, Q, R, S16P ⇒ (((Q ⇒ R) ⇒ S) ⇒ P)
P ⇒ ((Q ⇒ (R ⇒ S)) ⇒ P)
P ⇒ (Q ⇒ ((R ⇒ S) ⇒ P))
P ⇒ ((Q ⇒ R) ⇒ (S ⇒ P))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ P)))
((P ⇒ Q) ⇒ R) ⇒ (S ⇒ S)
(P ⇒ (Q ⇒ R)) ⇒ (S ⇒ S)
P ⇒ ((Q ⇒ R) ⇒ (S ⇒ S))
(P ⇒ Q) ⇒ (R ⇒ (S ⇒ S))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ S)))
(P ⇒ Q) ⇒ (R ⇒ (S ⇒ R))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ R)))
P ⇒ (Q ⇒ ((R ⇒ S) ⇒ Q))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ Q)))
5P, Q, R, S , T42
6P, Q, R, S, T, U132
Table of shortest tautological laws using implication alone, of increasing arity.

Reader’s feedback is welcome!

Don’t Repeat Yourself when Computing Relations

To say that I am "gobsmacked" is an understatement! The s(CASP) language fulfills a 40-year-old dream for a computer language that adheres to the "Don’t repeat yourself" philosophy.

s(CASP) was described in 2003 by Joaquin Arias, Manuel Carro, Elmer Salazar, Kyle Marple, and Andgopal Gupta. Constraint Answer Set Programming without Grounding. Here is a recent tutorial published for the language A Short Tutorial on s(CASP), a Goal-directed Execution of Constraint Answer Set Programs. And has been recently implemented in both Caio and SWI-PROLOG. And here is a recent review article s(CASP) + SWI-Prolog = 🔥.


Write your first s(CASP) program using the s(CASP) profile at https://swish.swi-prolog.org.


In this article I’ll describe by way of example, the kind of language that I have been looking for and show a small aspect of what s(CASP) can do that other languages can’t.

Forty years ago, in my undergraduate days, I was introduced to the logic programming language "Prolog". The premise of the language is that a Prolog program captures facts and rules and that Prolog ‘figures out’ how to order the computations required to answer a query. This Prolog Family Relationships example shows how Prolog doesn’t have a preferred direction of computation. The arguments are symmetric with regards to what is known and what is unknown.

As shown above, if we provide one argument Prolog will compute the other, or if we provide the "other", Prolog will compute the "one".

Dream Computer Language

My dream computer language has, at least, the following capabilities:

  • Capture data and computable relationships between data independent of the questions (or queries) that the programmer is currently aware of (unlike procedural languages but like DBMSs do for data)
  • Enter information once. For both data and computable relationships and allow any missing data to be computed. Another way of expressing this is that the language handles known and unknown arguments symmetrically, is indifferent to which arguments are known and which are unknown, creating a computation to find the missing arguments (as Prolog does for the computed relationship mother() and as SQL does for data)

Problem

I soon discovered that Prolog doesn’t keep up its indifference to the direction of computation for long. As soon as mathematical calculations are added to Prolog the paradigm of order-independent facts and rules stops working. Consider the GST in Prolog example Prolog program to calculate a 10% GST (or VAT).

As you can see from the above example, the Prolog language will only find a solution for one direction of computation. While the definition contains enough information to compute both directions to, and from Price, Prolog is unable to do so.

How does s(CASP) compare?

s(CASP) captures the pricingwithgst rule in a similar way to Prolog, but has a ‘super power’ it treats all the arguments to the rule symmetrically and therefore handles the GST example perfectly!

The s(CASP) program contains exactly the same information in the Prolog program and shows the symmetry of handling arguments that I have dreamed of!

Application

A programming language that allows the capturing of a computed relationship (GST being a trivial example) and then doesn’t care which arguments to the relationship are known and which are unknown can reduce the cost of building and maintaining digital models to be used for various purposes.

Following on from the GST example, it is almost certain that the code behind Australia’s GST Calculator web app contains two copies of the computed relationship between Price, GST, and Price exGST, one for each direction of calculation. If s(CASP) was behind the app then the computed relationship would be entered just once as a rule, and the two directions of computation would just be two different queries with different knowns and unknowns. s(CASP) would sequence a computation to find the missing values.

Functional Programming with SQL Query lambdas, functions and pipelines

Your input and feedback on this article are welcome on github.com/DavidPratten/sql-fp This article aims to add lambdas, functions and pipelines to the functional programming core of standard SQL, and thereby: separate transformation from … [Continue reading]

Composable Recursive Relational Queries

Your input and feedback on this article are welcome on github.com/DavidPratten/sql-fp Hierarchical and graph data may be transformed with relational queries that are recursive, iterative, and fixed-point. These are available in SQL through the … [Continue reading]

Aligning Real Estate Agent’s interests with those of the Vendor

The interests of property sellers (vendors) and the interests of their real estate agent can be better aligned. Firstly, this article shows how the "x% on sale price" commission model fails to reward agents for the effort required to find the … [Continue reading]

Table Valued Constrained Functions (TVCF) – Constraint Programming and SQL

I propose seamless integration of solvers into SQL via Table Valued Constrained Functions (TVCF). By "seamless", I mean that the SQL programmer would have to ask the query planner if a constraint solver was invoked to complete the query. A … [Continue reading]

I just found three bugs in SQLite!

SQLite is the most widely used and arguably the most rigorously tested database in the world. Today, the developers confirmed that valid queries that I created for the Rosella Model project exposed not one, not two, but three bugs hiding in the … [Continue reading]

Introducing tree “node elevation” to replace both “node depth and “node height”.

A tree's nodes may be assigned a depth and a height. If you would like to brush up on these concepts, then baeldung.com has a great explainer article Difference Between Tree Depth and Height. The difference may be summarised as MeasureMeasures … [Continue reading]

Finalist!

Celebrating Australian Underwater Running being chosen as a finalist in ABC RN Sporty program's "Invent-a-sport" competition! Here is the award broadcast starting around 6:20  the conversation is between host, Amanda Smith (AS), and judges Liz … [Continue reading]

Introducing Australian Underwater Running (AUR)

This is David Pratten's entry into the ABC's April, 2020 Invent a brand new sport and win a prize competition. Lets get ready for a post-COVID-19 world! When its time to come out and play, try Australian Underwater Running (AUR)! Play this … [Continue reading]

Applied Category Theory

Recently I reached out to Simon Willerton about applying Category Theory to Project Management models, here is the response. Putting Project Management models on a sound footing. Hi Simon, Thanks for your article on the Project Management Schedule … [Continue reading]

A relational language – Parasat

I am impressed by the logic language Picat and a recent presentation by Peter Alvaro "Three Things I Wish I Knew When I Started Designing Languages". Update 3: November 2022. The language MiniZinc turns out to fulfill the goals of Parasat … [Continue reading]

Using a Gantt Chart to Show Schedule Uncertainty

Temporary organisations (or projects) frequently work with uncertain timelines. Briefing senior management on the extent of uncertainty and progress towards reducing uncertainty is a crucial Project Management challenge. This article explores a … [Continue reading]

Formal and informal Latin script for Kazakh language

In 2017 President Nursultan Nazarbayev announced that Kazakhstan will fully transition from Cyrillic to Latin letters by 2025. I wrote this post in response. As my good friend Maktaxali taught me, we often find that "The caravan has left but the dogs … [Continue reading]

Underwater Running Survey

The Australian style of underwater running is unique in that it works irrespective of the runner's buoyancy and depth of water. This article surveys several different ways of running underwater. There is a beauty to this slow motion running in a … [Continue reading]