Large-size message construction for ETI, Validation of Lingua Cosmica

Paper number

IAC-12,A4,1,10,x13015

Author

Dr. Alexander Ollongren, Leiden University, The Netherlands

Year

2012

Abstract

In a sequence of papers on the topic of message construction for interstellar communication by means of a cosmic language, the present author has described the way his Lingua Cosmica system (LINCOS) can be applied. Constructive logic and the theory of types lie at the base of the system. The terms, logic clauses, rely on an environment of data built by means of a small set of declarators and make use of a limited set of low-level primitive operations, integrated in the system. Furthermore conclusions reached are formulated and verified in terms of system primitives and no recourse is taken to external means. The system is therefore self-contained and internal consistency is assured.
	Yet it is desirable to address the validation issue for LINCOS: have the results of sequences of reasoning (i.e. conclusions) a universal validity in some sense? The present contribution addresses this matter by considering LINCOS verifications of a selected set of relevant statements. The verifications are compared with proofs of the same statements obtained by means of an existing proof system in computer science. We use for that purpose the famous, reputable Coq system developed at INRIA in France and available in various releases on a wide range of data processing systems. In Coq, also based on constructive logic, proofs are carried out by means of high-level subsystems, and are in general not easily expressible in low-level primitives (opposite to the situation in Lingua Cosmica). 
	We show by representative examples that reasoning in Coq in terms of verifications can be transposed to equivalent reasoning in Lingua Cosmica – and the other way around. Thus relative validation is obtained as a step towards universal validity. An attractive side effect is that verifications in LINCOS are generally simpler and easier to understand than those in Coq.

Abstract document

IAC-12,A4,1,10,x13015.brief.pdf

Manuscript document

IAC-12,A4,1,10,x13015.pdf (🔒 authorized access only).

To get the manuscript, please contact IAF Secretariat.