Khunaji's Tautologies in Second-Order Logic

For the first time in the history of logic, Afzal al-Din al- Khunaji has found tautologies and contradictories among the verity and actuality propositions. These have been formalized and investigated in First-Order Logic and it has been shown that their perpetual truth requires the assumption of ‘the presupposed existence of nonexistence.’ In this paper, I investigate the tautologies in Second-Order Logic and show that there is no need to the aforementioned assumption, and they can be proved as theorems without any assumption in Second-Order Logic. But, the analysis of these tautologies in Second-Order Logic has its shortcomings; for example, the formalization of actuality I-propositions in many cases is contradictory. This shows that the analysis of the tautologies, whether in First- or Second-Order Logic, has shortcomings, which need to be removed.