text:
Front Matter Mimer, the Master Greyfell Curse of Gold Fafnir, the Dragon In Aegir's Kingdom Brunhild In Nibelungen Land Siegfried's Welcome Home Journey to Burgundyland Kriemhild's Dream How the Springtime Came War with the North-Kings Story of Balder Gunther Outwits Brunhild In Nibelungen Land Again Brunhild Welcomed Home Siegfried in Nibelungen Land How the Mischief Began Hunting in the Odenwald The Hoard Brought to Burgundy
Story of Siegfried - James Baldwin
The Curse of Gold
Forth then rode Siegfried, upon the beaming Greyfell, out into the broad mid-world. And the sun shone bright above him, and the air was soft and pure, and the earth seemed very lovely, and life a gladsome thing. And his heart was big within him as he thought of the days to come, of the deeds of love and daring, of the righting of many wrongs, of the people's praise, and the glory of a life well lived. And he wended his way back again toward the south and the fair lands of the Rhine. He left the barren moorlands behind him, and the pleasant farms and villages of the fruitful countryside, and after many days came once more to Regin's woodland dwelling. For he said to himself, "My old master is very wise; and he knows of the deeds that were done when yet the world was young, and my kin were the mightiest of men. I will go to him, and learn what grievous evil it is that he has so often vaguely hinted at."
Regin, when he saw the lad and the beaming Greyfell standing like a vision of light at his door, welcomed them most gladly, and led Siegfried into the inner room, where they sat down together amid the gold, and the gem stones, and the fine-wrought treasures there.
"Truly," said the master, "the days of my long waiting are drawing to a close, and at last the deed shall be done."
And the old look of longing came again into his eyes, and his pinched face seemed darker and more wrinkled than before, and his thin lips trembled with emotion as he spoke.
"What is that deed of which you speak?" asked Siegfried.
"It is the righting of a grievous wrong," answered Regin, "and the winning of treasures untold. Lo, many years have I waited for the coming of this day; and now my heart tells me that the hero so long hoped for is here, and the wisdom and the wealth of the world shall be mine."
"But what is the wrong to be righted?" asked Siegfried. "And what is this treasure that you speak of as your own?"
"Alas!" answered Regin, "the treasure is indeed mine; and yet wrongfully has it been withheld from me. But listen a while to a tale of the early days, and thou shalt know what the treasure is, and what is the wrong to be righted."
He took his harp and swept the strings, and played a soft, low melody which told of the dim past, and of blighted hopes, and of a nameless, never-satisfied yearning for that which might have been. And then he told Siegfried this story:
Regin's Story
When the earth was still very young, and men were feeble and few, and the Dwarfs were many and strong, the Asa-folk were wont ofttimes to leave their halls in heaven-towering Asgard in order to visit the new-formed mid-world, and to see what the short-lived sons of men were doing. Sometimes they came in their own god-like splendor and might; sometimes they came disguised as feeble men folk, with all man's weaknesses and all his passions. Sometimes Odin, as a beggar, wandered from one country to another, craving charity; sometimes, as a warrior clad in coat of mail, he rode forth to battle for the cause of right; or as a minstrel he sang from door to door, and played sweet music in the halls of the great; or as a huntsman he dashed through brakes and fens, and into dark forests, and climbed steep mountains in search of game; or as a sailor he embarked upon the sea, and sought new scenes in unknown lands. And many times did men folk entertain him unawares.
Once on a time he came to the mid-world in company with Hoenir and Loki; and the three wandered through many lands and in many climes, each giving gifts wherever they went. Odin gave knowledge and strength, and taught men how to read the mystic runes; Hoenir gave gladness and good cheer, and lightened many hearts with the glow of his comforting presence; but Loki had nought to give but cunning deceit and base thoughts, and he left behind him bitter strife and many aching breasts. At last, growing tired of the fellowship of men, the three Asas sought the solitude of the forest, and as huntsmen wandered long among the hills and over the wooded heights of Hunaland. Late one afternoon they came to a mountain stream at a place where it poured over a ledge of rocks, and fell in clouds of spray into a rocky gorge below. As they stood, and with pleased eyes gazed upon the waterfall, they saw near the bank an otter lazily making ready to eat a salmon which he had caught. And Loki, ever bent on doing mischief, hurled a stone at the harmless beast, and killed it. And he boasted loudly that he had done a worthy deed. And he took both the otter, and the fish which it had caught, and carried them with him as trophies of the day's success.
Just at nightfall the three huntsmen came to a lone farmhouse in the valley, and asked for food, and for shelter during the night.
"Shelter you shall have," said the farmer, whose name was Hreidmar, "for the rising clouds foretell a storm. But food I have none to give you. Surely huntsmen of skill should not want for food; since the forest teems with game, and the streams are full of fish."
Then Loki threw upon the ground the otter and the fish, and said, "We have sought in both forest and stream, and we have taken from them at one blow both flesh and fish. Give us but the shelter you promise, and we will not trouble you for food."
The farmer gazed with horror upon the lifeless body of the otter, and cried out, "This creature which you mistook for an otter, and which you have robbed and killed, is my son Oddar, who for mere pastime had taken the form of the furry beast. You are but thieves and murderers!"
Then he called loudly for help: and his two sons Fafnir and Regin, sturdy and valiant kin of the dwarf folk, rushed in, and seized upon the huntsmen, and bound them hand and foot; for the three Asas, having taken upon themselves the forms of men, had no more than human strength, and were unable to withstand them.
Then Odin and his fellows bemoaned their ill fate. And Loki said, "Wherefore did we foolishly take upon ourselves the likenesses of puny men? Had I my own power once more, I would never part with it in exchange for man's weaknesses."
And Hoenir sighed, and said, "Now, indeed, will darkness win: and the frosty breath of the Reimthursen giants will blast the fair handiwork of the sunlight and the heat; for the givers of life and light and warmth are helpless prisoners in the hands of these cunning and unforgiving jailers."
"Surely," said Odin, "not even the highest are free from obedience to heaven's behests and the laws of right. I, whom men call the Preserver of Life, have demeaned myself by being found in evil company; and, although I have done no other wrong, I suffer rightly for the doings of this mischief-maker with whom I have stooped to have fellowship. For all are known, not so much by what they are as by what they seem to be, and they bear the bad name which their comrades bear. Now I am fallen from my high estate. Eternal right is higher than I. And in the last Twilight of the gods I must needs meet the dread Fenris wolf, and in the end the world will be made new again, and the shining Balder will rule in sunlight majesty forever."
Then the Asas asked Hreidmar, their jailer, what ransom they should pay for their freedom; and he, not knowing who they were, said, "I must first know what ransom you are able to give."
"We will give any thing you may ask," hastily answered Loki.
Hreidmar then called his sons, and bade them strip the skin from the otter's body. When this was done, they brought the furry hide and spread it upon the ground; and Hreidmar said, "Bring shining gold and precious stones enough to cover every part of this otter skin. When you have paid so much ransom, you shall have your freedom."
"That we will do," answered Odin. "But one of us must have leave to go and fetch it: the other two will stay fast bound until the morning dawns. If, by that time, the gold is not here, you may do with us as you please."
Hreidmar and the two young men agreed to Odin's offer; and, lots being cast, it fell to Loki to go and fetch the treasure. When he had been loosed from the cords which bound him, Loki donned his magic shoes, which had carried him over land and sea from the farthest bounds of the mid-world, and hastened away upon his errand. And he sped with the swiftness of light, over the hills and the wooded slopes, and the deep dark valleys, and the fields and forests and sleeping hamlets, until he came to the place where dwelt the swarthy elves and the cunning dwarf Andvari. There the River Rhine, no larger than a meadow brook, breaks forth from beneath a mountain of ice, which the Frost giants and blind old Hoder, the Winter-king, had built long years before; for they had vainly hoped that they might imprison the river at its fountain head. But the baby brook had eaten its way beneath the frozen mass, and had sprung out from its prison, and gone on, leaping and smiling, and kissing the sunlight, in its ever-widening course towards Burgundy and the sea.
Loki came to this place, because he knew that here was the home of the elves who had laid up the greatest hoard of treasures ever known in the mid-world. He scanned with careful eyes the mountain side, and the deep, rocky caverns, and the dark gorge through which the little river rushed; but in the dim moonlight not a living being could he see, save a lazy salmon swimming in the quieter eddies of the stream. Any one but Loki would have lost all hope of finding treasure there, at least before the dawn of day; but his wits were quick, and his eyes were very sharp.
"One salmon has brought us into this trouble, and another shall help us out of it!" he cried.
Then, swift as thought, he sprang again into the air; and the magic shoes carried him with greater speed than before down the Rhine valley, and through Burgundyland, and the low meadows, until he came to the shores of the great North Sea. He sought the halls of old Ægir, the Ocean-king; but he wist not which way to go,—whether across the North Sea towards Isenland, or whether along the narrow channel between Britain land and the main. While he paused, uncertain where to turn, he saw the pale-haired daughters of old Ægir, the white-veiled Waves, playing in the moonlight near the shore. Of them he asked the way to Ægir's hall.
"Seven days' journey westward," said they, "beyond the green Isle of Erin, is our father's hall. Seven days' journey northward, on the bleak Norwegian shore, is our father's hall."
And they stopped not once in their play, but rippled and danced on the shelving beach, or dashed with force against the shore.
"Where is your mother Ran, the Queen of the Ocean?" asked Loki.
And they answered,—
"In the deep sea-caves
By the sounding shore,
In the dashing waves
When the wild storms roar,
In her cold green bowers
In the northern fiords,
She lurks and she glowers,
She grasps and she hoards,
And she spreads her strong net for her prey."
Loki waited to hear no more; but he sprang into the air, and the magic shoes carried him onwards over the water in search of the Ocean-queen. He had not gone far when his sharp eyes espied her, lurking near a rocky shore against which the breakers dashed with frightful fury. Half hidden in the deep dark water, she lay waiting and watching; and she spread her cunning net upon the waves, and reached out with her long greedy fingers to seize whatever booty might come near her.
When the wary queen saw Loki, she hastily drew in her net, and tried to hide herself in the shadows of an overhanging rock. But Loki called her by name, and said,—
"Sister Ran, fear not! I am your friend Loki, whom once you served as a guest in Ægir's gold-lit halls."
Then the Ocean-queen came out into the bright moonlight, and welcomed Loki to her domain, and asked, "Why does Loki thus wander so far from Asgard, and over the trackless waters?"
And Loki answered, "I have heard of the net which you spread upon the waves, and from which no creature once caught in its meshes can ever escape. I have found a salmon where the Rhine spring gushes from beneath the mountains, and a very cunning salmon he is, for no common skill can catch him. Come, I pray, with your wondrous net, and cast it into the stream where he lies. Do but take the wary fish for me, and you shall have more gold than you have taken in a year from the wrecks of stranded vessels."
"I dare not go," cried Ran. "A bound is set, beyond which I may not venture. If all the gold of earth were offered me, I could not go."
"Then lend me your net," entreated Loki. "Lend me your net, and I will bring it back to-morrow filled with gold."
"Much I would like your gold," answered Ran; "but I cannot lend my net. Should I do so, I might lose the richest prize that has ever come into my husband's kingdom. For three days, now, a gold-rigged ship, bearing a princely crew with rich armor and abundant wealth, has been sailing carelessly over these seas. To-morrow I shall send my daughters and the bewitching mermaids to decoy the vessel among the rocks. And into my net the ship, and the brave warriors, and all their armor and gold, shall fall. A rich prize it will be. No: I cannot part with my net, even for a single hour."
But Loki knew the power of flattering words.
"Beautiful queen," said he, "there is no one on earth, nor even in Asgard, who can equal you in wisdom and foresight. Yet I promise you, that, if you will but lend me your net until the morning dawns, the ship and the crew of which you speak shall be yours, and all their golden treasures shall deck your azure halls in the deep sea."
Then Ran carefully folded the net, and gave it to Loki.
"Remember your promise," was all that she said.
"An Asa never forgets," he answered.
And he turned his face again towards Rhineland; and the magic shoes bore him aloft, and carried him in a moment back to the ice mountain and the gorge and the infant river, which he had so lately left. The salmon still rested in his place, and had not moved during Loki's short absence.
Loki unfolded the net, and cast it into the stream. The cunning fish tried hard to avoid being caught in its meshes; but, dart which way he would, he met the skilfully woven cords, and these drew themselves around him, and held him fast. Then Loki pulled the net up out of the water, and grasped the helpless fish in his right hand. But, lo! as he held the struggling creature high in the air, it was no longer a fish, but the cunning dwarf Andvari.
"Thou King of the Elves," cried Loki, "thy cunning has not saved thee. Tell me, on thy life, where thy hidden treasures lie!"
The wise dwarf knew who it was that thus held him as in a vise; and he answered frankly, for it was his only hope of escape, "Turn over the stone upon which you stand. Beneath it you will find the treasure you seek."
Then Loki put his shoulder to the rock, and pushed with all his might. But it seemed as firm as the mountain, and would not be moved.
"Help us, thou cunning dwarf," he cried,—"help us, and thou shalt have thy life!"
The dwarf put his shoulder to the rock, and it turned over as if by magic, and underneath was disclosed a wondrous chamber, whose walls shone brighter than the sun, and on whose floor lay treasures of gold and glittering gem stones such as no man had ever seen. And Loki, in great haste, seized upon the hoard, and placed it in the magic net which he had borrowed from the Ocean-queen. Then he came out of the chamber; and Andvari again put his shoulder to the rock which lay at the entrance, and it swung back noiselessly to its place.
"What is that upon thy finger?" suddenly cried Loki. "Wouldst keep back a part of the treasure? Give me the ring thou hast!"
But the dwarf shook his head, and made answer, "I have given thee all the riches that the elves of the mountain have gathered since the world began. This ring I cannot give thee, for without its help we shall never be able to gather more treasures together."
And Loki grew angry at these words of the dwarf; and he seized the ring, and tore it by force from Andvari's fingers. It was a wondrous little piece of mechanism shaped like a serpent, coiled, with its tail in its mouth; and its scaly sides glittered with many a tiny diamond, and its ruby eyes shone with an evil light. When the dwarf knew that Loki really meant to rob him of the ring, he cursed it and all who should ever possess it, saying,—
"May the ill-gotten treasure that you have seized to-night be your bane, and the bane of all to whom it may come, whether by fair means or by foul! And the ring which you have torn from my hand, may it entail upon the one who wears it sorrow and untold ills, the loss of friends, and a violent death! The Norns have spoken, and thus it must be."
Loki was pleased with these words, and with the dark curses which the dwarf pronounced upon the gold; for he loved wrong-doing, for wrong-doing's sake, and he knew that no curses could ever make his own life more cheerless than it always had been. So he thanked Andvari for his curses and his treasures; and, throwing the magic net upon his shoulder, he sprang again into the air, and was carried swiftly back to Hunaland; and, just before the dawn appeared in the east, he alighted at the door of the farmhouse where Odin and Hoenir still lay bound with thongs, and guarded by Fafnir and Regin.
Then the farmer, Hreidmar, brought the otter's skin, and spread it upon the ground; and, lo! it grew, and spread out on all sides, until it covered an acre of ground. And he cried out, "Fulfil now your promise! Cover every hair of this hide with gold or with precious stones. If you fail to do this, then your lives, by your own agreement, are forfeited, and we shall do with you as we list."
Odin took the magic net from Loki's shoulder; and opening it, he poured the treasures of the mountain-elves upon the otter skin. And Loki and Hoenir spread the yellow pieces carefully and evenly over every part of the furry hide. But, after every piece had been laid in its place; Hreidmar saw near the otter's mouth a single hair uncovered; and he declared, that unless this hair, too, were covered, the bargain would be unfulfilled, and the treasures and lives of his prisoners would be forfeited. And the Asas looked at each other in dismay; for not another piece of gold, and not another precious stone, could they find in the net, although they searched with the greatest care. At last Odin took from his bosom the ring which Loki had stolen from the dwarf; for he had been so highly pleased with its form and workmanship, that he had hidden it, hoping that it would not be needed to complete the payment of the ransom. And they laid the ring upon the uncovered hair. And now no portion of the otter's skin could be seen. And Fafnir and Regin, the ransom being paid, loosed the shackles of Odin and Hoenir, and bade the three huntsmen go on their way.
Odin and Hoenir at once shook off their human disguises, and, taking their own forms again, hastened with all speed back to Asgard. But Loki tarried a little while, and said to Hreidmar and his sons,—
"By your greediness and falsehood you have won for yourselves the Curse of the Earth, which lies before you. It shall be your bane. It shall be the bane of every one who holds it. It shall kindle strife between father and son, between brother and brother. It shall make you mean, selfish, beastly. It shall transform you into monsters. The noblest king among men folk shall feel its curse. Such is gold, and such it shall ever be to its worshippers. And the ring which you have gotten shall impart to its possessor its own nature. Grasping, snaky, cold, unfeeling, shall he live; and death through treachery shall be his doom."
Then he turned away, delighted that he had thus left the curse of Andvari with Hreidmar and his sons, and hastened northward toward the sea; for he wished to redeem the promise that he had made to the Ocean-queen, to bring back her magic net, and to decoy the richly laden ship into her clutches.
No sooner were the strange huntsmen well out of sight than Fafnir and Regin began to ask their father to divide the glittering hoard with them.
"By our strength and through our advice," said they, "this great store has come into your hands. Let us place it in three equal heaps, and then let each take his share and go his way."
At this the farmer waxed very angry; and he loudly declared that he would keep all the treasure for himself, and that his sons should not have any portion of it whatever. So Fafnir and Regin, nursing their disappointment, went to the fields to watch their sheep; but their father sat down to guard his new-gotten treasure. And he took in his hand the glittering serpent-ring, and gazed into its cold ruby eyes: and, as he gazed, all his thoughts were fixed upon his gold; and there was no room in his heart for love toward his fellows, nor for deeds of kindness, nor for the worship of the All-Father. And behold, as he continued to look at the snaky ring, a dreadful change came over him. The warm red blood, which until that time had leaped through his veins, and given him life and strength and human feelings, became purple and cold and sluggish; and selfishness, like serpent's poison, took hold of his heart. Then, as he kept on gazing at the hoard which lay before him, he began to lose his human shape; his body lengthened into many scaly folds, and he coiled himself around his loved treasures,—the very likeness of the ring upon which he had looked so long.
When the day drew near its close, Fafnir came back from the fields with his herd of sheep, and thought to find his father guarding the treasure, as he had left him in the morning; but instead he saw a glittering snake, fast asleep, encircling the hoard like a huge scaly ring of gold. His first thought was that the monster had devoured his father; and, hastily drawing his sword, with one blow he severed the serpent's head from its body. And, while yet the creature writhed in the death-agony, he gathered up the hoard, and fled with it beyond the hills of Hunaland, until on the seventh day he came to a barren heath far from the homes of men. There he placed the treasures in one glittering heap; and he clothed himself in a wondrous mail-coat of gold that was found among them, and he put on the Helmet of Dread, which had once been the terror of the mid-world, and the like of which no man had ever seen; and then he gazed with greedy eyes upon the fateful ring, until he, too, was changed into a cold and slimy reptile,—a monster dragon. And he coiled himself about the hoard; and, with his restless eyes forever open, he gloated day after day upon his loved gold, and watched with ceaseless care that no one should come near to despoil him of it. This was ages and ages ago; and still he wallows among his treasures on the Glittering Heath, and guards as of yore the garnered wealth of Andvari.
When I, Regin, the younger brother, came back in the late evening to my father's dwelling, I saw that the treasure had been carried away; and, when I beheld the dead serpent lying in its place, I knew that a part of Andvari's curse had been fulfilled. And a strange fear came over me; and I left every thing behind me, and fled from that dwelling, never more to return. Then I came to the land of the Volsungs, where your father's fathers dwelt, the noblest king-folk that the world has ever seen. But a longing for the gold and the treasure, a hungry yearning, that would never be satisfied, filled my soul. Then for a time I sought to forget this craving. I spent my days in the getting of knowledge and in teaching men folk the ancient lore of my kin, the Dwarfs. I taught them how to plant and to sow, and to reap the yellow grain. I showed them where the precious metals of the earth lie hidden, and how to smelt iron from its ores,—how to shape the ploughshare and the spade, the spear and the battle-axe. I taught them how to tame the wild horses of the meadows, and how to train the yoke beasts to the plough; how to build lordly dwellings and mighty strongholds, and how to sail in ships across old Ægir's watery kingdom. But they gave me no thanks for what I had done; and as the years went by they forgot who had been their teacher, and they said that it was Frey who had given them this knowledge and skill. And I taught the young maidens how to spin and weave, and to handle the needle deftly,—to make rich garments, and to work in tapestry and embroidery. But they, too, forgot me, and said that it was Freyja who had taught them. Then I showed men how to read the mystic runes aright, and how to make the sweet beverage of poetry, that charms all hearts, and enlightens the world. But they say now that they had these gifts from Odin. I taught them how to fashion the tales of old into rich melodious songs, and with music and sweet-mouthed eloquence to move the minds of their fellow men. But they say that Bragi taught them this; and they remember me only as Regin, the elfin schoolmaster, or at best as Mimer, the master of smiths. At length my heart grew bitter because of the neglect and ingratitude of men; and the old longing for Andvari's hoard came back to me, and I forgot much of my cunning and lore. But I lived on and on, and generations of short-lived men arose and passed, and still the hoard was not mine; for I was weak, and no man was strong enough to help me.
Then I sought wisdom of the Norns, the weird women who weave the woof of every creature's fate.
"How long," asked I, "must I hope and wait in weary expectation of that day when the wealth of the world and the garnered wisdom of the ages shall be mine?"
And the witches answered, "When a prince of the Volsung race shall come who shall excel thee in the smithying craft, and to whom the All-Father shall give the Shining Hope as a helper, then the days of thy weary watching, shall cease."
"How long," asked I, "shall I live to enjoy this wealth and this wisdom, and to walk as a god among men? Shall I be long-lived as the Asa-folk, and dwell on the earth until the last Twilight comes?"
"It is written," answered Skuld, "that a beardless youth shall see thy death. But go thou now, and bide thy time."
Here Regin ended his story, and both he and Siegfried sat for a long time silent and thoughtful.
"I know what you wish," said Siegfried at last. "You think that I am the prince of whom the weird sisters spoke; and you would have me slay the dragon Fafnir, and win for you the hoard of Andvari."
"It is even so," answered Regin.
"But the hoard is accursed," said the lad.
"Let the curse be upon me," was the answer. "Is not the wisdom of the ages mine? And think you that I cannot escape the curse? Is there aught that can prevail against him who has all knowledge and the wealth of the world at his call?"
"Nothing but the word of the Norns and the will of the All-Father," answered Siegfried.
"But will you help me?" asked Regin, almost wild with earnestness. "Will you help me to win that which is rightfully mine, and to rid the world of a horrible evil?"
"Why is the hoard of Andvari more thine than Fafnir's?"
"He is a monster, and he keeps the treasure but to gloat upon its glittering richness. I will use it to make myself a name upon the earth. I will not hoard it away. But I am weak, and he is strong and terrible. Will you help me?"
"To-morrow," said Siegfried, "be ready to go with me to the Glittering Heath. The treasure shall be thine, and also the curse."
"And also the curse," echoed Regin.


text:
\section[Introduction]{Introduction}

The Axiom of Counting ($\mathrm{AxCount}$) was introduced by J. Barkley Rosser in \cite{ros78} and asserts that every finite set has the same cardinality as its own set of singletons. When added to Quine's `New Foundations' Set Theory ($\mathrm{NF}$) or Ronald Jensen's variant of $\mathrm{NF}$ that allows urelements ($\mathrm{NFU}$), this axiom proves the comprehension scheme for formulae which fail to be stratified only by virtue of the fact that well-defined types can not be assigned to variables which range only over natural numbers. In the nineteen seventies two natural variants of $\mathrm{AxCount}$ emerged: $\mathrm{AxCount}_\leq$ and $\mathrm{AxCount}_\geq$. $\mathrm{AxCount}_\leq$ asserts that a finite set is no bigger than its own set of singletons, while $\mathrm{AxCount}_\geq$ asserts that a finite set is no smaller than its own set of singletons. It quickly became apparent that many of the strong consequences of $\mathrm{AxCount}$ (over both $\mathrm{NF}$ and $\mathrm{NFU}$) also follow from $\mathrm{AxCount}_\leq$ \cite{hin75, fh09}. In contrast $\mathrm{AxCount}_\geq$ appears to be a much weaker assumption. This paper investigates the strength of $\mathrm{AxCount}_\geq$ over a theory, $\mathrm{NFU}^{-\mathrm{AC}}$, which can be viewed as both a subtheory of $\mathrm{NFU}$ (by which we mean Jensen's system \cite{jen69} supplemented with both with an axiom asserting the existence of a type-level pairing function and the Axiom of Choice) and $\mathrm{NF}$, and shows that this axiom proves the consistency of the Simple Theory of Types with Infinity ($\mathrm{TSTI}$).\\
\\
\indent In the context of $\mathrm{NF}$ very little is known about the relative strengths of the theories obtained by adding $\mathrm{AxCount}$, $\mathrm{AxCount}_\leq$ and $\mathrm{AxCount}_\geq$. Steven Orey \cite{ore64} shows that $\mathrm{NF}+\mathrm{AxCount}$ proves the consistency of $\mathrm{NF}$. In \cite{hin75} Roland Hinnion develops techniques that yield lower bounds on the consistency strengths of the theories $\mathrm{NF}+\mathrm{AxCount}$, $\mathrm{NF}+\mathrm{AxCount}_\leq$ and $\mathrm{NF}$ relative to subsystems of $\mathrm{ZFC}$. This paper provides a new lower bound on the consistency strength of $\mathrm{NF}+\mathrm{AxCount}_\geq$ relative to a well-understood $\mathrm{ZF}$-style theory. This lower bound is stronger than any known lower bound on the consistency strength of $\mathrm{NF}$.\\
\\
\indent There is much clearer picture of the relative strengths of the theories obtained by adding $\mathrm{AxCount}$, $\mathrm{AxCount}_\leq$ and $\mathrm{AxCount}_\geq$ to $\mathrm{NFU}$, largely thanks to Ronald Jensen's consistency proof of $\mathrm{NFU}$ \cite{jen69}. This consistency proof yields the exact strength of $\mathrm{NFU}$ relative to a subsystem of $\mathrm{ZFC}$, and Robert Solovay and Randall Holmes (unpublished) have also computed the exact strength of the theory $\mathrm{NFU}+\mathrm{AxCount}$ relative to a subsystem of $\mathrm{ZFC}$. The paper \cite{mck15} separates the consistency strengths of the theories $\mathrm{NFU}+\mathrm{AxCount}$, $\mathrm{NFU}+\mathrm{AxCount}_\leq$ and $\mathrm{NFU}+\mathrm{AxCount}_\geq$ by showing that $\mathrm{NFU}+\mathrm{AxCount}$ proves the consistency of $\mathrm{NFU}+\mathrm{AxCount}_\leq$, and $\mathrm{NFU}+\mathrm{AxCount}_\leq$ proves the consistency of $\mathrm{NFU}+\mathrm{AxCount}_\geq$. Here it is shown that $\mathrm{NFU}+\mathrm{AxCount}_\geq$ proves the consistency of $\mathrm{NFU}$ answering a question raised in \cite{mck15}.\\
\\
\indent This paper is only concerned with variants of Quine's `New Foundations' that are fortified with the Axiom of Infinity. It is interesting to note, however, that in \cite{ena06} Ali Enayat investigates the strengths of extensions of the theory $\mathrm{NFU}^{-\infty}$ that is obtained by adding the negation of the Axiom of Infinity to Jensen's modification of $\mathrm{NF}$. Robert Solovay has shown (unpublished) that $\mathrm{NFU}^{-\infty}$ is equiconsistent with the subsystem of arithmetic $I\Delta_0+\mathrm{exp}$. Both $\mathrm{AxCount}$ and $\mathrm{AxCount}_\leq$ are inconsistent with $\mathrm{NFU}^{-\infty}$. The theory $\mathrm{NFU}^{-\infty}+\mathrm{AxCount}_\geq$ is equivalent to the theory $\mathrm{NFUA}^{-\infty}$ which Enayat \cite{ena06} shows is equiconsistent with Peano Arithmetic ($\mathrm{PA}$).

\section[Background]{Background} \label{Sec:Background}

In this section we present the axioms of the theories $\mathrm{NFU}^{-\mathrm{AC}}$ and the Simple Theory of Types ($\mathrm{TSTI}$), and the extensions and subsystems of these theories that we will refer to in the next section of the paper. We also present some necessary facts related to the development of mathematics in $\mathrm{NFU}^{-\mathrm{AC}}$ and outline Roland Hinnion's technique of interpreting well-founded set theories in the set of equivalence classes of topped well-founded extensional relations in $\mathrm{NFU}^{-\mathrm{AC}}$. A detailed development of mathematics in an extension of $\mathrm{NFU}^{-\mathrm{AC}}$ can be found in the textbook \cite{hol98}. We also refer the reader to the monograph \cite{for95} for a treatment of advanced topics in the study of stratified set theories including extensions of $\mathrm{NFU}^{-\mathrm{AC}}$ and $\mathrm{TSTI}$.\\
\\
\indent Throughout this paper we will use $\mathcal{L}$ to denote the language of set theory: first-order logic endowed with the binary relation $\in$. We use $\mathcal{L}_{\mathrm{PA}}$ to denote the language of arithmetic: first-order logic endowed with binary function symbols $+$ and $\cdot$, and constant symbols $\mathbf{0}$ and $\mathbf{1}$. As usual we will write $\mathrm{PA}$ for the $\mathcal{L}_{\mathrm{PA}}$-theory that consists of all of the axioms of Peano Arithmetic. If $\mathcal{L}^\prime$ is a recursive language and $T$ is a recursively axiomatised $\mathcal{L}^\prime$-theory then we write $\mathrm{Con}(T)$ for the $\mathcal{L}_{\mathrm{PA}}$-formula which asserts that $T$ is consistent.\\
\\
\indent The Simple Theory of Types is the simplification of the underlying system of \cite{rw08} independently discovered by Frank Ramsey and Leon Chistwick. Following \cite{mat01} we use $\mathrm{TSTI}$ to denote the Simple Theory of Types fortified with the Axiom of Infinity. This theory is naturally axiomatised in the many-sorted language with sorts for each $n \in \mathbb{N}$.

\begin{Definitions1}
We use $\mathcal{L}_{\mathrm{TST}}$ to denote the $\mathbb{N}$-sorted language endowed with binary relation symbols $\in_n$ for each sort $n \in \mathbb{N}$. There are variables $x^n, y^n, z^n, \ldots$ for each sort $n \in \mathbb{N}$ and well-formed $\mathcal{L}_{\mathrm{TST}}$-formulae are built-up inductively from atomic formulae in the form $x^n \in_n y^{n+1}$ and $x^n = y^n$ using the connectives and quantifiers of first-order logic.
\end{Definitions1}

An $\mathcal{L}_{\mathrm{TST}}$-structure $\mathcal{M}$ consists of a function $M$ with domain $\mathbb{N}$ where $M(0), M(1), \ldots$ are the domains of the sorts, and a function $\in^\mathcal{M}$ with domain $\mathbb{N}$ such that for all $n \in \mathbb{N}$, $\in^\mathcal{M}(n) \subseteq M(n) \times M(n+1)$; we write $\mathcal{M}= \langle M, \in^\mathcal{M} \rangle$.

\begin{Definitions1}
We use $\mathrm{TSTI}$ to denote the $\mathcal{L}_{\mathrm{TST}}$-theory with axioms
\begin{itemize}
\item[](Extensionality) for all $n \in \mathbb{N}$,
$$\forall x^{n+1} \forall y^{n+1} (x^{n+1}= y^{n+1} \iff \forall z^n(z^{n} \in_n x^{n+1} \iff z^n \in_n y^{n+1})),$$
\item[](Comprehension) for all $n \in \mathbb{N}$ and for all well-formed $\mathcal{L}_{\mathrm{TST}}$-formulae $\phi(x^n, \vec{z})$,
$$\forall \vec{z} \exists y^{n+1} \forall x^n (x^n \in_n y^{n+1} \iff \phi(x^n, \vec{z}))$$
\item[](Infinity) $\exists x^1 \exists f^3(f^3: x^1 \longrightarrow x^1 \textrm{ is injective but not surjective})$.
\end{itemize}
\end{Definitions1}

If $n$ is a natural number with $n \geq 4$ then we use $\mathrm{TSTI}_n$ to denote the weakening of $\mathrm{TSTI}$ which only allows formulae to refer to objects with type $<n$.

\begin{Definitions1}
Let $n \in \mathbb{N}$ with $n \geq 4$. We use $\mathcal{L}_n$ to denote the $n$-sorted language endowed with binary relation symbols $\in_k$ for each sort $k < n-1$. There are variables $x^k, y^k, z^k, \ldots$ for each sort $k < n$ and well-formed $\mathcal{L}_n$-formulae are built-up inductively from atomic formulae in the form $x^k \in_k y^{k+1}$ where $k < n-1$, and $x^k = y^k$ where $k < n$, using the connectives and quantifiers of first-order logic.
\end{Definitions1}

If $n \in \mathbb{N}$ then we use $[n]$ to denote the set $\{i \in \mathbb{N} \mid i \leq n\}$ and we use $(n)$ to denote the set $\{i \in \mathbb{N} \mid i < n\}$. An $\mathcal{L}_n$-structure $\mathcal{M}$ consists of a function $M$ with domain $[n-1]$ where $M(0), \ldots, M(n-1)$ are the domains of the sorts, and a function $\in^\mathcal{M}$ with domain $(n-1)$ such that for all $k < n-1$, $\in^\mathcal{M}(k) \subseteq M(k) \times M(k+1)$; we write $\mathcal{M}= \langle M, \in^\mathcal{M} \rangle$.

\begin{Definitions1}
Let $n \in \mathbb{N}$ with $n \geq 4$. We use $\mathrm{TSTI}_n$ to denote the $\mathcal{L}_n$-theory with axioms
\begin{itemize}
\item[](Extensionality) for all $k < n-1$,
$$\forall x^{k+1} \forall y^{k+1} (x^{k+1}= y^{k+1} \iff \forall z^k(z^{k} \in_k x^{k+1} \iff z^k \in y^{k+1})),$$
\item[](Comprehension) for all $k < n-1$ and for all well-formed $\mathcal{L}_n$-formulae $\phi(x^k, \vec{z})$,
$$\forall \vec{z} \exists y^{k+1} \forall x^k (x^k \in_k y^{k+1} \iff \phi(x^k, \vec{z}))$$
\item[](Infinity) $\exists x^1 \exists f^3(f^3: x^1 \longrightarrow x^1 \textrm{ is injective but not surjective})$.
\end{itemize}
\end{Definitions1}

If $\sigma_0, \ldots, \sigma_m$ is a proof of a contradiction from $\mathrm{TSTI}$ then there exists an $n \in \mathbb{N}$ such that $\sigma_0, \ldots, \sigma_m$ is a proof of a contradiction from $\mathrm{TSTI}_n$. Combining this with the observation that there exists a binary Turing machine which on input $n \geq 4$ and $k$ decides whether the sentence with G\"{o}del number $k$ is an axiom of $\mathrm{TSTI}_n$ yields
\begin{equation}
\mathrm{PA} \vdash ((\forall n \geq 4) \mathrm{Con}(\mathrm{TSTI}_n) \iff \mathrm{Con}(\mathrm{TSTI}))
\end{equation}

\indent A formula in the language of set theory is said to be stratified if the formula can be turned into a well-formed formula of $\mathcal{L}_{\mathrm{TST}}$ by decorating variables and instances of $\in$ appearing in the formula with types. In 1937 Willard van Orman Quine proposed an axiomatisation of set theory, now dubbed `New Foundations' ($\mathrm{NF}$) after the title of \cite{qui37}, that appears to avoid the set theoretic paradoxes by restricting Cantor's unrestricted comprehension scheme to stratified formulae. In \cite{jen69} Ronald Jensen considers a weakening of $\mathrm{NF}$ that permits both sets and non-sets (urelements) in the domain of discourse. Jensen was able to show that this modification of $\mathrm{NF}$ is consistent relative to a weak subsystem of $\mathrm{ZFC}$ and, unlike $\mathrm{NF}$ (see \cite{spe53}), is consistent with both the Axiom of Choice and the negation of the Axiom of Infinity. In this paper we will stick to the convention of using $\mathrm{NFU}$ to denote Jensen's theory fortified by asserting the existence of a type-level pairing function, and by the Axiom of Choice. We will use $\mathrm{NFU}^{-\mathrm{AC}}$ to denote $\mathrm{NFU}$ minus the Axiom of Choice.

\begin{Definitions1}
We use $\mathcal{L}_{\mathrm{NFU}}$ to denote the extension of $\mathcal{L}$ obtained adding a unary predicate $\mathcal{S}$ and a binary function symbol $\langle \cdot, \cdot \rangle$.
\end{Definitions1}

The unary predicate $\mathcal{S}$ will be used to distinguish sets from urelements and $\langle \cdot, \cdot \rangle$ will act as a type-level pairing function. Before presenting the axioms of $\mathrm{NFU}^{-\mathrm{AC}}$ we first need to extend the notion of stratification to $\mathcal{L}_{\mathrm{NFU}}$-formulae.

\begin{Definitions1}
The terms of $\mathcal{L}_{\mathrm{NFU}}$ are built-up inductively from variables using the function $\langle \cdot, \cdot \rangle$. Let $\phi$ be an $\mathcal{L}_{\mathrm{NFU}}$-formula. We use $\mathbf{Term}(\phi)$ to denote the set of $\mathcal{L}_{\mathrm{NFU}}$-terms appearing in $\phi$. We say that $\sigma: \mathbf{Term}(\phi) \longrightarrow \mathbb{N}$ is a stratification of $\phi$ if for all terms $s$ and $t$ appearing in $\phi$,
\begin{itemize}
\item[(i)] if $s$ is a term appearing in $t$ then $\sigma(\textrm{`}t\textrm{'})= \sigma(\textrm{`}s\textrm{'})$,
\item[(ii)] if $s \in t$ is a subformula of $\phi$ then $\sigma(\textrm{`}t\textrm{'})= \sigma(\textrm{`}s\textrm{'})+1$,
\item[(iii)] if $s = t$ is a subformula of $\phi$ then $\sigma(\textrm{`}t\textrm{'})= \sigma(\textrm{`}s\textrm{'})$.
\end{itemize}
If there exists a stratification of $\phi$ then we say that $\phi$ is stratified.
\end{Definitions1}

\begin{Definitions1}
We use $\mathrm{NFU}^{-\mathrm{AC}}$ to denote the $\mathcal{L}_{\mathrm{NFU}}$-theory with axioms:
\begin{itemize}
\item[](Weak Extensionality) $\forall x \forall y(\mathcal{S}(x) \land \mathcal{S}(y) \Rightarrow (x=y \iff \forall z(z \in x \iff z \in y)))$
\item[](Stratified Comprehension) for all stratified $\mathcal{L}_{\mathrm{NFU}}$-formulae $\phi(x, \vec{z})$,
$$\forall \vec{z} \exists y (\mathcal{S}(y) \land \forall x(x \in y \iff \phi(x, \vec{z})))$$
\item[](Pairing) $\forall x \forall y \forall z \forall w(\langle x, y \rangle= \langle w, z \rangle \Rightarrow (x=w \land y=z))$
\end{itemize}
\end{Definitions1}

\begin{Definitions1}
We use $\mathrm{NFU}$ to denote the $\mathcal{L}_{\mathrm{NFU}}$-theory that obtained from $\mathrm{NFU}^{-\mathrm{AC}}$ by adding the Axiom of Choice.
\end{Definitions1}

Following \cite{hol98} and \cite{hol01} we have opted to include an axiom that asserts the existence of a type-level pairing function in our axiomatisation of $\mathrm{NFU}^{-\mathrm{AC}}$. We will indicate below how this pairing function implies that there exists a Dedekind infinite set. Without the Axiom of Choice, Jensen's theory \cite{jen69} fortified with an axiom asserting the existence of a Dedekind infinite set is not equivalent to $\mathrm{NFU}^{-\mathrm{AC}}$, however they do have the same consistency strength. One way of seeing this is to use \cite{jen69} combined with work done in \cite{mat01} to see that the Axiom of Choice can be consistently added to Jensen's theory \cite{jen69} fortified with an axiom asserting the existence of a Dedekind infinite set. In the presence of both the Axiom of Choice and an axiom asserting the existence of a Dedekind infinite set, Jensen's theory \cite{jen69} is equipped with a type-level pairing function that can be used in instances of the comprehension scheme. This shows that $\mathrm{NFU}^{-\mathrm{AC}}$ and $\mathrm{TSTI}$ have exactly the same consistency strength:

\begin{Theorems1} \label{Th:ConsistencyStregthOfNFU}
(Jensen) $\mathrm{Con}(\mathrm{NFU}^{-\mathrm{AC}}) \iff \mathrm{Con}(\mathrm{TSTI})$. \Square
\end{Theorems1}

The set theory $\mathrm{NF}$ can be obtained from $\mathrm{NFU}^{-\mathrm{AC}}$ by adding an axiom which says that everything is a set.

\begin{Definitions1}
We use $\mathrm{NF}$ to denote the $\mathcal{L}_{\mathrm{NFU}}$-theory obtained from $\mathrm{NFU}^{-\mathrm{AC}}$ by adding the axiom
\begin{equation} \label{Eq:EveryObjectIsASet}
\forall x(\mathcal{S}(x))
\end{equation}
\end{Definitions1}

It should be noted that we could have axiomatised $\mathrm{NF}$, as is done in \cite{qui37}, in the language $\mathcal{L}$. In the presence of (\ref{Eq:EveryObjectIsASet}) the symbol $\mathcal{S}$ becomes redundant and the Weak Extensionality axiom reduces to the usual extensionality axiom for set theory. It follows from \cite{spe53} and \cite{qui45} that any model of $\mathrm{NF}$ can be expanded to a model with a pairing function $\langle \cdot, \cdot\rangle$ that satisfies the Pairing Axiom and can be used in instances of the Stratified Comprehension scheme without raising types. It should also be noted that \cite{spe53} shows that the Axiom of Choice is inconsistent with $\mathrm{NFU}^{-\mathrm{AC}}$ plus (\ref{Eq:EveryObjectIsASet}).\\
\\
\indent Stratified Comprehension in the theory $\mathrm{NFU}^{-\mathrm{AC}}$ guarantees the existence of a universal set which we denote $V$. The fact that the function $x \mapsto \langle x, x \rangle$ is injective but not surjective implies that $V$ is Dedekind infinite. Cardinal and ordinal numbers in $\mathrm{NFU}^{-\mathrm{AC}}$ are defined to be equivalence classes of equipollent sets and equivalence classes of isomorphic well-orderings respectively. If $X$ is a set then we use $|X|$ to denote the cardinal number such that $X \in |X|$. Stratified Comprehension ensures that both the set of all ordinals ($\mathrm{NO}$) and the set of all cardinals ($\mathrm{NC}$) exist. We use $\mathrm{NCI}$ to denote the set of infinite cardinals. The least cardinal number, denoted $\mathbf{0}$, is the set of all sets and urelements that have no members. We use $\iota$ denote the function $x \mapsto \{x\}$. Equipped with a successor operation ($S$) we are able to define the natural numbers ($\mathbb{N}$) as the smallest inductive set:
$$S(x)= \{y \mid (\exists z \in y)(y \backslash \iota z \in x)\}$$
$$\mathbb{N}= \bigcap \{x \mid (\mathbf{0} \in x) \land (\forall y \in x)(S(y) \in x)\}.$$
Define $+$ and $\cdot$ on $\mathbb{N}$ by: for all $k, m, n \in \mathbb{N}$,
$$k+m= n \textrm{ if there exists } x \in k \textrm { and } y \in m \textrm{ with } x \cap y = \emptyset \textrm{ and } n= |x \cup y|$$
$$k \cdot m= n \textrm{ if there exists } x \in k \textrm{ and } y \in m \textrm{ such that } |x \times y|= n.$$
By letting $\mathbf{1}= S(\mathbf{0})$ we obtain an $\mathcal{L}_\mathrm{PA}$-structure $\langle \mathbb{N}, +, \cdot, \mathbf{0}, \mathbf{1} \rangle$ that is a model of $\mathrm{PA}$. If $n$ is a concrete natural number then by adjoining the sets $\mathcal{P}(\mathbb{N}), \mathcal{P}^2(\mathbb{N}), \ldots, \mathcal{P}^{n-1}(\mathbb{N})$ to the structure $\langle \mathbb{N}, +, \cdot, \mathbf{0}, \mathbf{1} \rangle$ we obtain a structure that is a model of $n^{\textrm{th}}$ order arithmetic.\\
\\
\indent This interpretation of Peano Arithmetic allows $\mathrm{NFU}^{-\mathrm{AC}}$ to describe the syntax of recursive languages. If $\mathcal{L}^\prime$ is a recursive language then expressions in $\mathcal{L}^\prime$ can be coded as elements of $\mathbb{N}$, called a G\"{o}del coding, in such a way so as effective properties of $\mathcal{L}^\prime$ expressions are definable by arithmetic (and therefore stratified) $\mathcal{L}_{\mathrm{NFU}}$-formulae. Given a recursive language $\mathcal{L}^\prime$ we assume that a G\"{o}del coding of $\mathcal{L}^\prime$ has been fixed and we write $\ulcorner \phi \urcorner$ for the G\"{o}del code of $\phi$. We will often omit the corners and equate a formula $\phi$ with its G\"{o}del code. In \cite{hin75} Hinnion shows that if an $\mathcal{L}$-structure $\mathcal{M}$ is a set then there is a stratified formula $\mathrm{Sat}_\mathcal{L}(\phi, a, \mathcal{M})$ which says that $\phi$ is an $\mathcal{L}$-formulae, $a$ is sequence of elements of $M$ that agrees with the arity of $\phi$ and $\mathcal{M}$ satisfies $\phi[a]$. If $\mathcal{L}^\prime$ is a recursive language then Hinnion's definition of satisfaction for $\mathcal{L}$-structures can easily be extended to define a ternary stratified formula $\mathrm{Sat}_{\mathcal{L}^\prime}$ which expresses satisfaction in an $\mathcal{L}^\prime$-structure. Using the stratified formulae $\mathrm{Sat}_{\mathcal{L}_\mathrm{PA}}$ one can see that $\mathrm{NFU}^{-\mathrm{AC}}$ proves the single sentence which asserts that the structure $\langle \mathbb{N}, +, \cdot, \mathbf{0}, \mathbf{1} \rangle$ is a model of $\mathrm{PA}$. And, moreover, for any concrete natural number $n$, $\mathrm{NFU}^{-\mathrm{AC}}$ proves the single sentence which asserts that the structure $\langle \mathcal{P}^{n-1}(\mathbb{N}), \ldots, \mathcal{P}(\mathbb{N}), \mathbb{N}, +, \cdot, \mathbf{0}, \mathbf{1} \rangle$ is a model of $n^\textrm{th}$ order arithmetic. If $\mathcal{M}$ is a set structure in a recursive language $\mathcal{L}^\prime$, $\phi$ is an $\mathcal{L}^\prime$-formula and $a$ is a sequence of elements of $\mathcal{M}$ then we will write $\mathcal{M} \models \phi[a]$ instead of $\mathrm{Sat}_{\mathcal{L}^\prime}(\phi, a, \mathcal{M})$.\\
\\
\indent The following definition mirrors the definition of an initial ordinal in $\mathrm{ZFC}$:

\begin{Definitions1}
We say that an ordinal $\alpha$ is initial if
$$(\forall \delta < \alpha)(|\{\beta \mid \beta < \delta\}| < |\{\beta \mid \beta < \alpha\}|).$$
We use $\omega$ to denote the first initial ordinal, $\omega_1$ to denote the least initial ordinal $>\omega$, $\omega_2$ to denote the least initial ordinal $>\omega_1$, etc.
\end{Definitions1}

In $\mathrm{ZFC}$ cardinals correspond to initial ordinals. It is important to note that in $\mathrm{NFU}^{-\mathrm{AC}}$ this coincidence does not occur. If $R$ is a binary relation then we will write $\mathrm{Dom}(R)$ for $\mathrm{dom}(R) \cup \mathrm{rng}(R)$.

\begin{Definitions1}
Let $\alpha$ be an ordinal. Define
$$\mathrm{Card}(\alpha)= |\mathrm{Dom}(R)| \textrm{ where } R \in \alpha.$$
For all $n \in \mathbb{N}$, define $\aleph_n= \mathrm{Card}(\omega_n)$.
\end{Definitions1}

\indent One unorthodox feature of $\mathrm{NFU}^{-\mathrm{AC}}$ is the fact that it proves that there are sets, for example $V$, which are not the same size as their own set of singletons. This motivates the introduction of the $T$ operation which is defined on cardinals, ordinals and equivalence classes of isomorphic well-founded relations, and the definition of Cantorian and strongly Cantorian sets. If $R$ is a relation then we use $[R]$ to denote the set of all relations isomorphic to $R$. If $F$ is a function and $X$ is a set then we write $F``X$ for the set of all things that can be obtained by applying $F$ to an element of $X$.

\begin{Definitions1}
We say that a set $X$ is Cantorian if $|X|= |\iota``X|$. We say a set $X$ is strongly Cantorian if the restriction of the map $\iota$ to $X$ witnesses the fact that $|X|= |\iota``X|$.
\end{Definitions1}

\begin{Definitions1}
If $X$ is a set then define
$$T(|X|)= |\iota``X|.$$
If $R$ is a well-founded relation then define
$$T([R])= [\{\langle \iota x, \iota y \rangle \mid \langle x, y \rangle \in R\}].$$
\end{Definitions1}

The $T$ operation commutes with the functions $+$ and $\cdot$ defined on $\mathbb{N}$ and is the identity on $\mathbf{0}$ and $\mathbf{1}$. Since both $T``\mathbb{N}$ and $T^{-1}``\mathbb{N}$ contain $\mathbf{0}$ and are closed under $S$, it follows that $T``\mathbb{N}= \mathbb{N}$. Therefore the $T$ operation is an automorphism of the interpretation of arithmetic in a model of $\mathrm{NFU}^{-\mathrm{AC}}$. The Axiom of Counting ($\mathrm{AxCount}$) asserts that this automorphism is the identity:
\begin{itemize}
\item[]($\mathrm{AxCount}$) $(\forall n \in \mathbb{N})(T(n)=n)$
\end{itemize}
This axiom was first introduced by J. Barkley Rosser in \cite{ros78} in order to facilitate induction in $\mathrm{NF}$. Steve Orey's \cite{ore64} shows that $\mathrm{NF}+\mathrm{AxCount}$ proves $\mathrm{Con}(\mathrm{NF})$. As part of \cite{hol01}, which also initiates the comparison of extensions of $\mathrm{NFU}$ with subsystems and extensions of $\mathrm{ZFC}$, Randall Holmes investigates the strength of the theory $\mathrm{NFU}+\mathrm{AxCount}$ in terms of which infinite cardinals this theory proves exist. In \cite{for77} Thomas Forster identifies two natural weakenings of $\mathrm{AxCount}$:
\begin{itemize}
\item[]($\mathrm{AxCount}_\leq$) $(\forall n \in \mathbb{N})(n \leq T(n))$
\item[]($\mathrm{AxCount}_\geq$) $(\forall n \in \mathbb{N})(n \geq T(n))$
\end{itemize}
Many of the strong consequences of $\mathrm{AxCount}$ also follow from the weaker assumption $\mathrm{AxCount}_\leq$. For example, \cite{hin75} shows that $\mathrm{NF}+\mathrm{AxCount}_\leq$ proves the consistency of Zermelo Set Theory. And \cite{fh09} shows that if $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\leq$ is consistent then so is $\mathrm{NFU}^{-\mathrm{AC}}+ (\textrm{the function on } \mathbb{N} \textrm{ defined by } n \mapsto V_n \textrm{ exists})$. In contrast it is not known if $\mathrm{NF}+\mathrm{AxCount}_\geq$ proves the consistency of Zermelo Set Theory. And the assertion that the function on $\mathbb{N}$ defined by $n \mapsto V_n$ exists proves $\mathrm{AxCount}_\leq$. The relative strengths of $\mathrm{AxCount}$, $\mathrm{AxCount}_\leq$ and $\mathrm{AxCount}_\geq$ over $\mathrm{NFU}$ is studied in \cite{mck15}:

\begin{Theorems1} \label{Th:VariantsOfAxCountOverNFU}
\begin{itemize}
\item[(I)] $\mathrm{NFU}+\mathrm{AxCount} \vdash \mathrm{Con}(\mathrm{NFU}+\mathrm{AxCount}_\leq)$
\item[(II)] $\mathrm{NFU}+\mathrm{AxCount}_\leq \vdash \mathrm{Con}(\mathrm{NFU}+\mathrm{AxCount}_\geq)$
\end{itemize}
\end{Theorems1}

\cite{mck15} also provides evidence which appears to indicate that, over $\mathrm{NFU}$, $\mathrm{AxCount}_\geq$ is weak.

\begin{Theorems1} \label{Th:EvidenceThatAxCountGEQIsWeak}
There is a model of $\mathrm{NFU}+\mathrm{AxCount}_\geq$ which believes that $\mathrm{NCI}$ is finite.
\end{Theorems1}

\cite{mat01} shows that $\mathrm{TSTI}$ is equiconsistent with the set theory $\mathrm{MOST}$ that is a subsystem of $\mathrm{ZFC}$ that includes the Axiom of Choice. The fact that equiconsistencies between $\mathrm{MOST}$ and $\mathrm{TSTI}$, and $\mathrm{TSTI}$ and $\mathrm{NFU^{-\mathrm{AC}}}$ show that these theories have the same arithmetic yields the following strong equiconsistency:

\begin{Theorems1} \label{Th:StrongConsistencyOfChoiceWithNFU}
(Jensen, Mathias)
$$\mathrm{Con}(\mathrm{NFU}^{-\mathrm{AC}}) \iff \mathrm{Con}(\mathrm{NFU}).$$
Moreover, if $\phi$ is an $\mathcal{L}_\mathrm{PA}$-sentence then
$$\mathrm{NFU}^{-\mathrm{AC}} \vdash \phi \textrm{ if and only if } \mathrm{NFU} \vdash \phi.$$
\end{Theorems1}

It follows from Theorem \ref{Th:StrongConsistencyOfChoiceWithNFU} that any occurrence of ``$\mathrm{NFU}$" in Theorem \ref{Th:VariantsOfAxCountOverNFU} can be replaced by ``$\mathrm{NFU}^{-\mathrm{AC}}$".\\
\\
\indent In \cite{hin75} Hinnion shows that subsystems of $\mathrm{ZFC}$ can be interpreted in substructures of the set of equivalence classes of isomorphic topped well-founded extensional relations in $\mathrm{NF}$. Hinnion's techniques have since been established (see \cite{hol98}, \cite{hol01} and \cite{solXX}) as the standard method for proving lower bounds on the consistency strength of extensions of $\mathrm{NFU}^{-\mathrm{AC}}$ relative to subsystems and extensions of $\mathrm{ZFC}$.

\begin{Definitions1} \label{Df:BFEXT}
A structure $\langle A, R \rangle$, where $R$ is a binary relation, is a $\mathrm{BFEXT}$ if
\begin{itemize}
\item[(i)] $\mathrm{Dom}(R)= A$,
\item[(ii)] $\forall B((B \neq \emptyset \land B \subseteq A) \Rightarrow (\exists b \in B)(\forall c \in B) \neg (\langle c, b \rangle \in R))$,
\item[(iii)] $(\forall a, b \in A)(a=b \iff \forall c(\langle c, a \rangle \in R \iff \langle c, b \rangle \in R))$.
\end{itemize}
We say that a binary relation $R$ is a $\mathrm{BFEXT}$ if $\langle \mathrm{Dom}(R), R \rangle$ is a $\mathrm{BFEXT}$.
\end{Definitions1}

\begin{Definitions1} \label{Df:Segment}
Let $\langle A, R \rangle$ be a $\mathrm{BFEXT}$. If $a \in A$ then define
$$\mathrm{seg}_R(a)= R \upharpoonright \bigcap \{B \subseteq A \mid (a \in B \land (\forall b \in B)(\forall c \in B)(\langle c, b \rangle \in R \Rightarrow c \in B))\}.$$
\end{Definitions1}

\begin{Definitions1}
$$\Omega= \{R \mid (R \textrm{ is a } \mathrm{BFEXT}) \land (\exists a \in \mathrm{Dom}(R))(R= \mathrm{seg}_R(a))\}$$
\end{Definitions1}

The fact that $\Omega$ is defined by a stratified set abstract shows that $\mathrm{NFU}^{-\mathrm{AC}}$ proves that $\Omega$ is a set. If $R \in \Omega$ then the $a \in \mathrm{Dom}(R)$ with $R= \mathrm{seg}_R(a)$ is unique--- we will use $\mathds{1}_R$ to denote this element. We will sometimes call $[R]$ the type of $R$.

\begin{Definitions1}
The structure $\langle \mathrm{BF}, \mathcal{E} \rangle$ is defined by
$$\mathrm{BF}= \{[R] \mid R \in \Omega\}$$
$$\mathcal{E}= \{\langle [R], [S] \rangle \in \mathrm{BF} \times \mathrm{BF} \mid (\exists a \in \mathrm{Dom}(S))(R \cong \mathrm{seg}_S(a) \land \langle a, \mathds{1}_S \rangle \in S)\}.$$
\end{Definitions1}

\begin{Theorems1} \label{Th:BFisWellFoundedAndExtensional}
(Hinnion) The structure $\langle \mathrm{BF}, \mathcal{E} \rangle$ is well-founded and extensional. \Square
\end{Theorems1}

A consequence of this theorem is that if $\mathfrak{a}$ is an equivalence class of isomorphic BFEXTs then $\mathrm{seg}_{\mathcal{E}}(\mathfrak{a})$ is a BFEXT. The BFEXTs represented by $\mathfrak{a}$ are related to $\mathrm{seg}_{\mathcal{E}}(\mathfrak{a})$ by the $T$ operation.

\begin{Lemma1} \label{Th:RelationshipBetweenBFEXTAndSeg}
(Hinnion) If $\mathfrak{a} \in \mathrm{BF}$ then $[\mathrm{seg}_{\mathcal{E}}(\mathfrak{a})]= T^2(\mathfrak{a})$. \Square
\end{Lemma1}

By considering rank initial segments of the structure $\langle \mathrm{BF}, \mathcal{E} \rangle$ Hinnion builds models of subsystems of $\mathrm{ZFC}$.

\begin{Definitions1}
Let $S$ be a well-founded extensional relation. Define
$$S^0= \{a \in \mathrm{Dom}(S) \mid \neg(\exists b \in \mathrm{Dom}(S))(\langle b, a \rangle \in S)\}$$
$$S^{\alpha+1}= \{a \in \mathrm{Dom}(S) \mid \forall b(\langle b, a\rangle \in S \Rightarrow b \in S^\alpha)\}$$
$$S^\lambda= \bigcup_{\alpha<\lambda} S^\alpha \textrm{ for limit } \lambda.$$
\end{Definitions1}

\noindent Note that for well-founded extensional $S$, the formula `$x=S^\alpha$' is stratified and admits a stratification which assigns the same type to the variables `$x$' and `$\alpha$'.

\begin{Definitions1}
For an ordinal $\alpha$, we use $M_\alpha$ to denote $\mathcal{E}^{\omega+\alpha}$.
\end{Definitions1}

\noindent Note that $M_0= \{[R] \mid |\mathrm{Dom}(R)|< \aleph_0\}$ and $|M_0|= \aleph_0$.\\
\\
\indent One of the achievements of \cite{hin75}, which we mentioned above, was to show that if $\mathrm{AxCount}_\leq$ holds in $\mathrm{NF}$ then the single sentence asserting that $M_{\omega}$ is a model of Zermelo Set Theory is provable. Even though the setting of \cite{hin75} is $\mathrm{NF}$, Hinnion's argument can also be carried out in the weaker theory $\mathrm{NFU}^{-\mathrm{AC}}$ (see \cite{hol98} and \cite{solXX}). Combining this with the work in \cite{mat01} on the consistency strength of $\mathrm{TSTI}$ we note the following weak version of Hinnion's result which we will use in the next section.

\begin{Theorems1} \label{Th:HinnionLowerBoundOnStrengthOfAxCountLEQ}
(Hinnion) $\mathrm{NFU}^{-\mathrm{AC}} + \mathrm{AxCount}_\leq \vdash \mathrm{Con}(\mathrm{TSTI})$. \Square
\end{Theorems1}

\section[$\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ proves the consistency of $\mathrm{TSTI}$]{$\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ proves the consistency of $\mathrm{TSTI}$}

In this section I will show that $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ proves the consistency of $\mathrm{TSTI}$. The main tool used to prove this result is the technique, developed in \cite{hin75}, of using the class of topped well-founded extensional relations in $\mathrm{NFU}^{-\mathrm{AC}}$ to interpret well-founded set theories. It follows from Theorem \ref{Th:HinnionLowerBoundOnStrengthOfAxCountLEQ} that if $\mathrm{AxCount}$ holds in $\mathrm{NFU}^{-\mathrm{AC}}$ then $\mathrm{Con}(\mathrm{TSTI})$ holds. In light of this, all we need to prove is that the theory $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq+\neg \mathrm{AxCount}$ proves the consistency of $\mathrm{TSTI}$.\\
\\
\indent Let $\mathcal{M}$ be a model of $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq+ \neg\mathrm{AxCount}$. The proof will show that there is an elementary $\mathcal{L}_{\mathrm{PA}}$-substructure $\mathcal{A}$ of $\langle \mathbb{N}^\mathcal{M}, +^\mathcal{M}, \cdot^\mathcal{M}, \mathbf{0}^\mathcal{M}, \mathbf{1}^\mathcal{M} \rangle$ that satisfies $\mathrm{Con}(\mathrm{TSTI})$. It then follows from the elementarity of $\mathcal{A}$ that $\mathcal{M}$ satisfies $\mathrm{Con}(\mathrm{TSTI})$. The fact that $\mathcal{A}$ satisfies $\mathrm{Con}(\mathrm{TSTI})$ will be obtained by showing that for every $n \in \mathcal{A}$, there is a set substructure of $\langle \mathrm{BF}, \mathcal{E} \rangle$ that is a model of $\mathrm{TSTI}_n$. The structure $\mathcal{A}$ is obtained by considering the fixed points of $T$ acting on $\mathbb{N}^\mathcal{M}$. The following Lemma is proved in the  theory $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq+ \neg\mathrm{AxCount}$:

\begin{Lemma1} \label{Th:FixedPointSetOfTIsInitialSegment}
If $n \in \mathbb{N}$ is such that $T(n)=n$ then for all $m \leq n$, $T(m)=m$.
\end{Lemma1}

\begin{proof}
Suppose that there are $n, m \in \mathbb{N}$ with $m < n$, $T(n)=n$ and $T(m) < m$. But then $n-m \in \mathbb{N}$ and
$$T(n-m)= T(n) - T(m) = n - T(m) > n - m$$
which contradicts $\mathrm{AxCount}_\geq$.
\Square
\end{proof}

\begin{Definitions1}
Define $\mathcal{A}= \langle A, +^\mathcal{A}, \cdot^\mathcal{A}, \mathbf{0}^\mathcal{A}, \mathbf{1}^\mathcal{A} \rangle$ to be the $\mathcal{L}_\mathrm{PA}$-substructure of\\
$\langle \mathbb{N}^\mathcal{M}, +^\mathcal{M}, \cdot^\mathcal{M}, \mathbf{0}^\mathcal{M}, \mathbf{1}^\mathcal{M} \rangle$ with domain
$$A=\{n \in \mathbb{N}^\mathcal{M} \mid \mathcal{M} \models (T(n)=n)\}.$$
\end{Definitions1}

Note that since $A \subseteq \mathbb{N}^\mathcal{M}$, $A \neq \mathbb{N}$, $\mathbf{0}^\mathcal{M} \in A$ and $A$ is closed under $S^\mathcal{M}$ it follows that $A$ is not a set of $\mathcal{M}$.

\begin{Lemma1}
The $\mathcal{L}_\mathrm{PA}$-structure $\langle \mathbb{N}^\mathcal{M}, +^\mathcal{M}, \cdot^\mathcal{M}, \mathbf{0}^\mathcal{M}, \mathbf{1}^\mathcal{M} \rangle$ is a proper elementary end-extension of $\mathcal{A}$.
\end{Lemma1}

\begin{proof}
Lemma \ref{Th:FixedPointSetOfTIsInitialSegment} implies that  $\langle \mathbb{N}^\mathcal{M}, +^\mathcal{M}, \cdot^\mathcal{M}, \mathbf{0}^\mathcal{M}, \mathbf{1}^\mathcal{M} \rangle$ is an end-extension of $\mathcal{A}$. It follows from the fact that $\mathcal{M} \models \neg \mathrm{AxCount}$ that $A \neq \mathbb{N}^\mathcal{M}$. That $\mathcal{A} \prec \langle \mathbb{N}^\mathcal{M}, +^\mathcal{M}, \cdot^\mathcal{M}, \mathbf{0}^\mathcal{M}, \mathbf{1}^\mathcal{M} \rangle$ follows since $T^\mathcal{M}$ is an automorphism of the structure  $\langle \mathbb{N}^\mathcal{M}, +^\mathcal{M}, \cdot^\mathcal{M}, \mathbf{0}^\mathcal{M}, \mathbf{1}^\mathcal{M} \rangle$ and $\mathrm{PA}$ has definable Skolem functions.
\Square
\end{proof}

We now turn to showing that for all $n \in A$, $\mathcal{A}$ satisfies $\mathrm{Con}(\mathrm{TSTI}_n)$. This will be achieved by working in $\mathcal{M}$ and showing that there is an $n \in \mathbb{N}$ such that $T(n) < n$ and there exists a set model of $\mathrm{TSTI}_n$ in the structure $\langle \mathrm{BF}, \mathcal{E} \rangle$. From this point on we work inside $\mathcal{M}$.

\begin{Definitions1}
If $\kappa$ is a cardinal then define
$$2^{\kappa}= \left\{\begin{array}{ll}
|\mathcal{P}(X)| & \textrm{if there exists a set } X \textrm{ with } |\iota``X|= \kappa\\
\emptyset & \textrm{otherwise}
\end{array} \right)$$
\end{Definitions1}

\noindent This modification of the usual definition of cardinal exponentiation has the property that the function $\kappa \mapsto 2^\kappa$ is definable by a stratified formula which admits a stratification that assigns the same type to the result and the argument of the function. The following result shows that this exponentiation operation possesses the strictly inflationary property that we intuitively associate with cardinal exponentiation.

\begin{Lemma1} \label{Th:ExpInflationary}
Let $\kappa$ be a cardinal. If $2^{\kappa} \neq \emptyset$ then $\kappa < 2^{\kappa}$.
\end{Lemma1}

\begin{proof}
The usual proof of Cantor's Theorem yields for all $X$, $|\iota``X| < |\mathcal{P}(X)|$ and this proof only appeals stratified instances of comprehension.
\Square
\end{proof}

\begin{Definitions1}
Define $\beth: \mathbb{N} \longrightarrow \mathrm{NC}$ by
$$\beth(0)= \aleph_0$$
$$\beth(n+1)= \left\{\begin{array}{ll}
2^{\beth(n)} & \textrm{if } \beth(n) \in \mathrm{NC}\\
\emptyset & \textrm{if } \beth(n)= \emptyset
\end{array}\right.$$
\end{Definitions1}

\noindent Note that stratified comprehension ensures that $\beth$ is a set. The following results are proved or adapted from results proved in \cite{hin75}.

\begin{Lemma1}
If $2^\kappa \neq \emptyset$ then $T(2^\kappa)=2^{T(\kappa)}$.
\end{Lemma1}

\begin{proof}
This follows immediately from the fact that for all $X$, $|\iota``\mathcal{P}(X)|= |\mathcal{P}(\iota``X)|$.
\Square
\end{proof}

\begin{Lemma1} \label{Th:TFunctionOnBeths}
Let $n \in \mathbb{N}$. If $\beth(n) \neq \emptyset$ then $\beth(T(n)) = T(\beth(n))$.
\end{Lemma1}

\begin{proof}
We prove this by induction on $n$. It holds for $n=0$. Suppose that the Lemma holds for $n$. Suppose that $\beth(n+1) \neq \emptyset$. Therefore $\beth(n) \neq \emptyset$ and so $\beth(T(n))= T(\beth(n))$. So,
$$\beth(T(n+1))= \beth(T(n)+1)= 2^{\beth(T(n))}= 2^{T(\beth(n))}= T(2^{\beth(n)})= T(\beth(n+1)).$$
\Square
\end{proof}

\begin{Lemma1} \label{Th:ConditionForPowerOf2ToExist}
If $\kappa \leq T(|V|)$ then $2^\kappa \neq \emptyset$.
\end{Lemma1}

\begin{proof}
Let $X \in \kappa$ and let $f: X \longrightarrow \iota``V$ be an injection. Let $B= \mathrm{rng}(f)$ and let $A= \bigcup B$. Therefore $|\iota``A|= \kappa$. \Square
\end{proof}

\begin{Lemma1} \label{Th:ExistenceOfNonStandardN}
There exists an $n \in \mathbb{N}$ with $T(n) < n$ such that $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$.
\end{Lemma1}

\begin{proof}
If $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$ for all $n \in \mathbb{N}$, then we are done since $\mathrm{AxCount}$ fails and $\mathrm{AxCount}_\geq$ holds. Suppose that $n+1$ is least such that $\beth(n+1) = \emptyset$ or $\beth(n+1) \nleq T^4(|V|)$. If $T(n+1)= n+1$ then $T(n)= n$. And, $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$. But then, by Lemma \ref{Th:ConditionForPowerOf2ToExist}, $\beth(n+1) \neq \emptyset$. And, by Lemma \ref{Th:TFunctionOnBeths}, $T(\beth(n+1))= \beth(n+1)$. So, $\beth(n+1) \leq |V|$ implies that $\beth(n+1) \leq T^4(|V|)$, which contradicts our assumptions. Therefore $T(n+1) < n+1$ and $T(n) < n$. Since $n+1$ was least such that $\beth(n+1) = \emptyset$ or $\beth(n+1) \nleq T^4(|V|)$, it follows that $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$.
\Square
\end{proof}

\begin{Lemma1} \label{Th:SizeOfM}
Let $n \in \mathbb{N}$. If $\beth(T(n)) \neq \emptyset$ then $|M_n| \leq \beth(T(n))$.
\end{Lemma1}

\begin{proof}
The assertion `$\beth(T(n)) \neq \emptyset \Rightarrow |M_n| \leq \beth(T(n))$' is stratified, so we can prove it by induction. The base case holds because $|M_0|= \aleph_0$. Suppose that the Lemma holds for some $n \in \mathbb{N}$ and assume that $\beth(T(n+1)) \neq \emptyset$. Note that if $\mathfrak{a} \in M_{n+1}$ then $\{\mathfrak{b} \mid \langle \mathfrak{b}, \mathfrak{a} \rangle \in \mathcal{E}\} \subseteq M_n$. The map $g: \iota``M_{n+1} \longrightarrow \mathcal{P}(M_n)$ defined by $\{\mathfrak{a}\} \mapsto \{\mathfrak{b} \mid \langle \mathfrak{b}, \mathfrak{a} \rangle \in \mathcal{E}\}$ is injective. Therefore $T(|M_{n+1}|) \leq |\mathcal{P}(M_n)|$. Now, $|\iota``M_n|= T(|M_n|)$, therefore $2^{T(|M_n|)}= |\mathcal{P}(M_n)|$. We also know that $2^{\beth(T(n))} \neq \emptyset$. And so,
$$T(|M_{n+1}|) \leq 2^{T(|M_n|)} \leq 2^{T(\beth(T(n)))}= T(2^{\beth(T(n))})= T(\beth(T(n+1))).$$
\Square
\end{proof}

\begin{Lemma1} \label{Th:EveryBFEXTisT2}
Let $n \in \mathbb{N}$ be such that $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$. If $\mathfrak{a} \in M_n$ then there is a $\mathfrak{b} \in \mathrm{BF}$ such that $\mathfrak{a}= T^2(\mathfrak{b})$.
\end{Lemma1}

\begin{proof}
Let $n \in \mathbb{N}$ be such that $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$. Let $\mathfrak{a} \in M_n$. Therefore $\mathrm{Dom}(\mathrm{seg}_\mathcal{E}(\mathfrak{a})) \subseteq M_n$, and so $|\mathrm{Dom}(\mathrm{seg}_\mathcal{E}(\mathfrak{a}))| \leq |M_n|$. Since $T(n) \leq n$, we know that $\beth(T(n)) \neq \emptyset$. Therefore, by Lemma \ref{Th:SizeOfM},
$$|\mathrm{Dom}(\mathrm{seg}_\mathcal{E}(\mathfrak{a}))| \leq \beth(T(n)) \leq \beth(n) \leq T^4(|V|).$$
Let $f: \mathrm{Dom}(\mathrm{seg}_\mathcal{E}(\mathfrak{a})) \longrightarrow \iota^4``V$ be an injection. Let $A= \bigcup^4 \mathrm{rng}(f)$ and define $S \subseteq A \times A$ by
$$\langle x, y \rangle \in S \textrm{ if and only if } \langle f^{-1}(\iota^4 x), f^{-1}(\iota^4 y) \rangle \in \mathrm{seg}_\mathcal{E}(\mathfrak{a}).$$
Let $\mathfrak{b}= [S]$. By Lemma \ref{Th:RelationshipBetweenBFEXTAndSeg} we have
$$T^2(\mathfrak{a})= [\mathrm{seg}_\mathcal{E}(\mathfrak{a})]= T^4(\mathfrak{b}).$$
Therefore $\mathfrak{a}= T^2(\mathfrak{b})$.
\Square
\end{proof}

\begin{Lemma1} \label{Th:KeyCompLemma}
Let $n \in \mathbb{N}$ be such that $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$. If $B \subseteq M_n$ then there exists $\mathfrak{d} \in M_{n+1}$ such that for all $\mathfrak{b} \in M_n$,
$$\langle \mathfrak{b}, \mathfrak{d} \rangle \in \mathcal{E} \textrm{ if and only if } \mathfrak{b} \in B.$$
\end{Lemma1}

\begin{proof}
Let $B \subseteq M_n$. It follows from Lemma \ref{Th:EveryBFEXTisT2} that for all $\mathfrak{b}$, there exists $\mathfrak{b}^\prime \in \mathrm{BF}$ such that $\mathfrak{b}= T^2(\mathfrak{b}^\prime)$. Therefore, by Lemma \ref{Th:RelationshipBetweenBFEXTAndSeg}, for all $\mathfrak{b} \in \mathrm{BF}$, $\mathfrak{b}= [\mathrm{seg}_{\mathcal{E}}(\mathfrak{b}^\prime)]$. Define
$$S= \left(\bigcup \{ \mathrm{seg}_{\mathcal{E}}(\mathfrak{b}^\prime) \mid T^2(\mathfrak{b}^\prime) \in B\}\right) \cup \{\langle \mathfrak{b}^\prime, V \rangle \mid T^2(\mathfrak{b}^\prime) \in B\}.$$
Now, $S \in \Omega$ and so let $\mathfrak{d}= [S]$. It is clear that $\mathfrak{d} \in M_{n+1}$ and for all $\mathfrak{b} \in M_n$,
$$\langle \mathfrak{b}, \mathfrak{d} \rangle \in \mathcal{E} \textrm{ if and only if } \mathfrak{b} \in B.$$
\Square
\end{proof}

Equipped with these results we are now in a position to show that $\mathcal{M}$ satisfies $\mathrm{Con}(\mathrm{TSTI})$.

\begin{Lemma1}
$\mathcal{M} \models \mathrm{Con}(\mathrm{TSTI})$.
\end{Lemma1}

\begin{proof}
Suppose that $\mathcal{M} \models \neg \mathrm{Con}(\mathrm{TSTI})$. Therefore
$$\mathcal{M} \models (\exists k \geq 4) \neg \mathrm{Con}(\mathrm{TSTI}_k).$$
Since the arithmetic of $\mathcal{M}$ is elementarily equivalent to $\mathcal{A}$ this implies
$$\mathcal{A} \models (\exists k \geq 4) \neg \mathrm{Con}(\mathrm{TSTI}_k).$$
Let $k \in A$ be such that $\mathcal{A} \models \neg \mathrm{Con}(\mathrm{TSTI}_k)$. Since $\mathcal{A}$ is an elementary submodel of the arithmetic of $\mathcal{M}$, this means that $\mathcal{M} \models \neg \mathrm{Con}(\mathrm{TSTI}_k)$. Note that $\mathcal{M} \models (T(k)=k)$.\\
Now, work inside $\mathcal{M}$. Let $n \in \mathbb{N}$ be such that $T(n) < n$, $\beth(n) \neq \emptyset$ and $\beth(n) \leq T^4(|V|)$. Lemma \ref{Th:ExistenceOfNonStandardN} ensures that there exists an $n \in \mathbb{N}$ with these properties. Note that for all $i \leq n$, $\beth(i) \neq \emptyset$ and $\beth(i) \leq T^4(|V|)$. We will build a set model of $\mathrm{TSTI}_{n+1}$. Since $k < n$ this will yield a contradiction. Let $D: [n] \longrightarrow V$ be defined by $D(i)= M_i$ for all $i \leq n$. Let $\in^\mathcal{D}: (n) \longrightarrow V$ be defined by $\in^\mathcal{D}(i)= \mathcal{E} \upharpoonright M_i \times M_{i+1}$. Note that Stratified Comprehension ensures that the functions $D$ and $\in^\mathcal{D}$ are sets. The structure $\mathcal{D}= \langle D, \in^\mathcal{D} \rangle$ is an $\mathcal{L}_{n+1}$-structure.\\
We need to show that $\mathcal{D} \models \mathrm{TSTI}_{n+1}$. To see that $\mathcal{D} \models (\textrm{Extensionality})$ observe that the structure $\langle \mathrm{BF}, \mathcal{E} \rangle$ is extensional (Theorem \ref{Th:BFisWellFoundedAndExtensional}) and for each $i \leq n$, $\langle \mathrm{BF}, \mathcal{E} \rangle$ is an end-extension of $\langle M_i, \mathcal{E} \rangle$.\\
We now turn to showing that $\mathcal{D} \models (\textrm{Comprehension})$. Let $i < n$. Let $\phi(x^i, z_0^{j_0}, \ldots, z_{m-1}^{j_{m-1}})$ be an $\mathcal{L}_{n+1}$-formula (according to $\mathcal{M}$). We need to show that
$$\mathcal{D} \models \forall \vec{z} \exists y^{i+1} \forall x^i(x^i \in_i y^{i+1} \iff \phi(x^i, \vec{z})).$$
Let $\vec{\mathfrak{a}}: (m) \longrightarrow \bigcup \mathrm{rng}(D)$ be a sequence such that for all $0 \leq l < m$, $\vec{\mathfrak{a}}(l) \in D(j_l)$. Let
$$B= \{\mathfrak{b} \in M_i \mid \exists \vec{\mathfrak{c}}((\vec{\mathfrak{c}}: [m] \longrightarrow V) \land (\vec{\mathfrak{c}}(0)= \mathfrak{b}) \land (\forall l \in (m))(\vec{\mathfrak{c}}(l+1)= \vec{\mathfrak{a}}(l)) \land (\mathcal{D} \models \phi[\vec{\mathfrak{c}}]))\}.$$
Stratified Comprehension ensures that $B$ is a set. Clearly $B \subseteq M_{i+1}$. By Lemma \ref{Th:KeyCompLemma} there exists $\mathfrak{d} \in M_{i+1}$ such that for all $\mathfrak{b} \in M_i$,
$$\begin{array}{ccccc}
\mathcal{D} \models (\mathfrak{b} \in_i \mathfrak \mathfrak{d}) & \textrm{if and only if} & \langle \mathfrak{b}, \mathfrak{d} \rangle \in \mathcal{E} & \textrm{if and only if} & \textrm{there exists } \vec{\mathfrak{c}}: [m] \longrightarrow V \textrm{ with}\\
& & & & \vec{\mathfrak{c}}(0)= \mathfrak{b} \textrm{ and } (\forall l \in (m))(\vec{\mathfrak{c}}(l+1)= \vec{\mathfrak{a}}(l))\\
& & & & \textrm{and } \mathcal{D} \models \phi[\vec{\mathfrak{c}}]
\end{array}$$
This shows that Comprehension holds in $\mathcal{D}$.\\
Finally, we need to show that $\mathcal{D} \models (\textrm{Infinity})$. Let
$$R=\{\langle i, j \rangle \mid i, j \in \mathbb{N} \land i < j\} \cup \{\langle i, V \rangle \mid i \in \mathbb{N}\}.$$
The relation $R$ is a BFEXT with $R= \mathrm{seg}_R(V)$, therefore $R \in \Omega$. Let $\mathfrak{a}= [R]$. Note that $\mathfrak{a} \in M_1$. Let $\phi(x, y)$ be the $\mathcal{L}$-formula
$$(x= \langle z_1, z_2 \rangle) \land (z_1, z_2 \in y) \land (z_2= z_1 \cup \{z_1\}).$$
Let
$$B= \{ \mathfrak{b} \in M_0 \mid \exists \vec{\mathfrak{c}} ((\vec{\mathfrak{c}}: (2) \longrightarrow V) \land (\vec{\mathfrak{c}}(0)= \mathfrak{b}) \land (\vec{\mathfrak{c}}(1)= \mathfrak{a}) \land (\langle M_1, \mathcal{E} \rangle \models \phi[\vec{\mathfrak{c}}]))\}.$$
Stratified Comprehension ensures that $B$ is a set. We also have that $B \subseteq M_3$. Using Lemma \ref{Th:KeyCompLemma} we can find $\mathfrak{d} \in M_3$ such that for all $\mathfrak{b} \in M_2$,
$$\langle \mathfrak{b}, \mathfrak{d} \rangle \in \mathcal{E} \textrm{ if and only if } \mathfrak{b} \in B.$$
The point $\mathfrak{d}$ in $\mathcal{D}$ is an injective function that witnesses that $\mathfrak{a}$ is Dedekind infinite.\\
This shows that $\mathcal{M} \models \mathrm{Con}(\mathrm{TSTI}_{n+1})$. Since $k < n+1$, $\mathcal{M} \models \mathrm{Con}(\mathrm{TSTI}_k)$, which is a contradiction.
\Square
\end{proof}

Since $\mathcal{M}$ was an arbitrary model of $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq+ \neg\mathrm{AxCount}$ this proves:

\begin{Theorems1} \label{Th:MainTheorem}
$\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq \vdash \mathrm{Con}(\mathrm{TSTI})$. \Square
\end{Theorems1}

\noindent Combined with Theorem \ref{Th:ConsistencyStregthOfNFU} this shows that the theory $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ has strictly stronger consistency strength than the theory $\mathrm{NFU}^{-\mathrm{AC}}$.

\begin{Coroll1} \label{Th:AxCountGEQStrictlyStrongerOverNFU}
$\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq \vdash \mathrm{Con}(\mathrm{NFU}^{-\mathrm{AC}})$. \Square
\end{Coroll1}

Again, Theorem \ref{Th:StrongConsistencyOfChoiceWithNFU} allows any occurrence of ``$\mathrm{NFU}^{-\mathrm{AC}}$" in Corollary \ref{Th:AxCountGEQStrictlyStrongerOverNFU} to be replaced with ``$\mathrm{NFU}$". The following from \cite{mck15} still remains open:

\begin{Quest1}
What is the exact consistency strength of $\mathrm{NFU}+\mathrm{AxCount}_\geq$ relative to a subsystem of $\mathrm{ZFC}$?
\end{Quest1}

Since the theory $\mathrm{NF}$ can be viewed as an extension of the theory $\mathrm{NFU}^{-\mathrm{AC}}$, Theorem \ref{Th:MainTheorem} also yields:

\begin{Coroll1}
$\mathrm{NF}+\mathrm{AxCount}_\geq \vdash \mathrm{Con}(\mathrm{TSTI})$. \Square
\end{Coroll1}

\bibliographystyle{alpha}

redpajama_set_name: RedPajamaArXiv


Where to buy andoer 60cm 23 6 all metal aluminum alloy video track slider dolly rail stabilizer max load 6kg for canon nikon sony dslr cam camera camcorder intl, this product is a well-liked item in 2019. this product is a new item sold by TOMTOP store and shipped from Hong Kong SAR China. Andoer 60cm/23.6" All Metal Aluminum Alloy Video Track Slider Dolly Rail Stabilizer Max. Load 6kg for Canon Nikon Sony DSLR Cam Camera Camcorder - intl can be purchased at lazada.sg having a cheap cost of SGD52.26 (This price was taken on 25 May 2018, please check the latest price here). do you know the features and specifications this Andoer 60cm/23.6" All Metal Aluminum Alloy Video Track Slider Dolly Rail Stabilizer Max. Load 6kg for Canon Nikon Sony DSLR Cam Camera Camcorder - intl, let's see the important points below.
Made of strong and durable aluminum alloy.
60cm double-tracks rail for soundless, smooth and fast sliding effect.
With 1/4" screw on the plate, and a 1/4" to 3/8" convertible screw.
With 1/4" and 3/8" screw on the track.
Height adjustable supporting foot with non-slip rubber.
For detailed product information, features, specifications, reviews, and guarantees or another question that is certainly more comprehensive than this Andoer 60cm/23.6" All Metal Aluminum Alloy Video Track Slider Dolly Rail Stabilizer Max. Load 6kg for Canon Nikon Sony DSLR Cam Camera Camcorder - intl products, please go straight to the seller store that will be coming TOMTOP @lazada.sg.
TOMTOP is often a trusted shop that already practical knowledge in selling Tripods & Monopods products, both offline (in conventional stores) and internet based. many of the clientele are incredibly satisfied to get products from your TOMTOP store, that can seen with all the many 5 star reviews given by their clients who have obtained products from the store. So there is no need to afraid and feel focused on your product or service not up to the destination or not according to what exactly is described if shopping in the store, because has lots of other buyers who have proven it.
Moreover TOMTOP also provide discounts and product warranty returns in the event the product you purchase won't match whatever you ordered, of course using the note they provide. As an example the product that we are reviewing this, namely "Andoer 60cm/23.6" All Metal Aluminum Alloy Video Track Slider Dolly Rail Stabilizer Max. Load 6kg for Canon Nikon Sony DSLR Cam Camera Camcorder - intl", they dare to offer discounts and product warranty returns if your products they sell don't match precisely what is described.
So, if you want to buy or look for Andoer 60cm/23.6" All Metal Aluminum Alloy Video Track Slider Dolly Rail Stabilizer Max. Load 6kg for Canon Nikon Sony DSLR Cam Camera Camcorder - intl however recommend you purchase it at TOMTOP store through marketplace lazada.sg.
Why would you buy Andoer 60cm/23.6" All Metal Aluminum Alloy Video Track Slider Dolly Rail Stabilizer Max. Load 6kg for Canon Nikon Sony DSLR Cam Camera Camcorder - intl at TOMTOP shop via lazada.sg?
Obviously there are several advantages and benefits available while shopping at lazada.sg, because lazada.sg is a trusted marketplace and have a good reputation that can give you security coming from all kinds of online fraud. Excess lazada.sg in comparison with other marketplace is lazada.sg often provide attractive promotions for example rebates, shopping vouchers, free postage, and quite often hold flash sale and support that is fast and that's certainly safe. and what I liked happens because lazada.sg can pay on the spot, that has been not there in every other marketplace.


Last year, in celebration of SFX's 150th issue, we invited Russell T Davies to meet Verity Lambert, the original, pioneering producer of Doctor Who. It was a conversation we were privileged to be part of – Verity was by then one of the most significant and influential figures in British television, but had clearly lost none of her love for the phenomenon she had helped to birth (nor her talent for expressing frank, insightful opinion). She had a reputation for taking no prisoners, but welcomed us into her London home with warmth and charm to spare. In tribute to this legend of the television industry – and someone who was very much the mother of our favourite Time Lord – we present another chance to read the interview that originally appeared in SFX 150.
Verity, can you see a throughline from your Doctor Who to Russell's?
V: And I think they should be there. That's what's so clever about it. Most of the writers seem to be members of the Doctor Who Appreciation Society (laughs) so they've kind of lived and immersed themselves in Doctor Who. What you've managed to do is extract the essence of what was there, and at the same time bring it into 2006.
R: We've really taken it back to the '60s. All the structures that were put up inbetween are gone – the Time Lords and all that pompery, which I love, as a fan, but when you look at what you were doing in 1963, it was just so open.
V: You see, I didn't have any Time Lords at all. He was a mystery. That's why he was Doctor Who. Had he stolen this thing called a TARDIS? He didn't know how to work it – was he an absent-minded professor? Was he a criminal? Was he on the run?
Did you have a background for him worked out in your own heads?
V: No, I had no idea. We had this mystery character, who didn't have a background, who was just there, and could have been anything, and that was actually more interesting than trying to give him a background. At that point we wanted him to be a mystery. If he'd stolen the ship, were they in the hands of some lunatic?
V: Finally after about two days of headbashing I said we're not going to explain it! There is no explanation, and if we don't give one, people will accept it. I mean, it's bigger on the inside – how can you ever explain that? So we didn't. And nobody ever asked!
R: No, you never do. It's just like Narnia and the wardrobe.
Russell, do you and David Tennant know stuff about the Doctor that the audience don't?
R: No, not particularly. We know roughly a lot of the stories for season four. We have conversations about big Doctor stories that are to come, stuff that will challenge him, certain key episodes that will look at him in a new light. But no, we don't talk it to death. We just get on and do it.
V: I was the youngest producer in the drama department by a long way. And the only woman, at that point. Most of the people in the drama department couldn't understand why I'd been hired anyway. They used to ask me if I'd slept with [Head of Drama] Sydney Newman to get the job.
R: They asked you out loud?
V: Out loud! Yes, one or two people, after they'd had a few in the club. So I had to overcome all that – not that I minded, particularly, because I was pretty thick-skinned.
R: Did you have a thick skin, though, or did you grow it?
V: I think I always had one. When you're 26 years old you think you can do anything. I had a huge opportunity and because you don't really know anything you think you know everything.
R: They must have thought you were so…radical! I just imagine everyone else at the time were middle-aged men wearing demob suits! You were wild, you lot! 26 year old woman, gay Asian director… they must have thought you were bananas!
Did you have the final decision on who should play the Doctor?
V: Yes, absolutely. I thought about Bill because he did this thing called The Army Game where he played this ghastly Sergeant Major, and then I saw This Sporting Life, where he played this failed rugby league talent scout… and he was so touching in it. And I thought well, here's an actor who can combine two things, because I always thought that Doctor Who should be dangerous, at the same time as touching and lovable as well.
So is that the same for you, Russell, when you're casting the Doctor?
R: I think it's there with him. I think a lot of his fun and japes are an act. He plays it as an act.
Would you cast an older Doctor?
R: No. There's no question of it, because it's 12 hours a day, 6 days a week for 9 months of the year. If we cast someone who was 50 they'd be dead now.
V: I think that nowadays you don't really want an older Doctor. I think the fact that these guys are hip and modern is very good, and the audience likes that. I don't think that they would respond to some older man. I thought David Tennant was a really, really good idea. I have to be very honest and say I wasn't quite so sure about Christopher. I think he's a wonderful actor, but I wasn't sure that he was right, and I felt when I was watching it – although I enjoyed it – that he was not completely comfortable.
R: Oh, he was. He loved it. I think he was playing an uncomfortableness with people, with humans.
V: I prefer David Tennant. I just think he's so winning.
R: It's hard to find those – there are very few leading men like that, with the energy to carry a show like that. If he'd said no, I wonder to this day what we would have done.
V: I tell you, the real revelation for me was Billie Piper.
R: For all of us, for all of us. Bless her!
V: I thought she was just brilliant. The thing about her is that she never stops, she always plays it for real, which is just wonderful.
R: She does that 100% of the day, every day. Never had a bad day with her. Everybody has a tired day or a sleepy day, even the best actors in the world – but never with her. Quite extraordinary, the commitment.
Verity, you also introduced the Daleks. They were a phenomenon, weren't they?
V: I remember going down to rehearsal, when we had the first Daleks, and everyone including me wanted to get inside them and run them around. There was just something about them.
Did you get inside them?
V: Yes! Of course I did!
R: I never have (laughs) Too big. I think I'd get stuck! I think I'd still be in it now!
V: There was just something magical about them.
R: There is something, isn't there? They just draw the eye. It's literally true – everyone gets excited when the Daleks are on set.
The amazing thing is that it still works, and these are kids who haven't grown up with Doctor Who.
R: I knew it would. I was the one saying don't change a detail. The proportions and the shape are exactly the same. There was a lovely Bryan Hitch design of flying, circular Daleks, but it was just a droid – Star Wars is full of them. That doesn't scare me. But there's something brilliant about that shape. It's inbuilt with me, because they scared me when I was three years old, but to see it working again, with kids, is just extraordinary. I used to draw them as a kid compulsively. But of course they all went into the void, so you'll never see them again (laughs).
Verity, is it true you were in talks to bring back Doctor Who in the early '90s?
V: No, they did, and at that time I wanted Peter Cook to play the Doctor.
R: Oh, wow! That would have been wonderful.
V: But then I thought well, I've done this. I was quite young when I made it, and I think it needs younger people – it needs people who are in touch with young people.
R: I'm 43… but I'm one of the gays! Hooray! We go down the disco!
R: Yes, it was gorgeous!
V: I love the way you relate it to what's happening. I loved the one with Zoe Wanamaker, where she'd had all that plastic surgery. I like the way you get in the kind of follies that occur today. It's not just Daleks and Cybermen. It's to do with some of the really idiotic things that happen in the world we live in. I think one of the problems with Doctor Who is that it went on for a very long time, and sometimes you need a gap, time to take a deep breath and say hold on a minute, things have changed around us, and we need to incorporate those things.
R: I'm not just saying this because you're here, but like I said, a lot of it was also about taking it back to the 60s… no Time Lords, proper people as companions who had histories and real lives, seeing the wonder of the Tardis, travelling into the future and the past… And that's what you did. There have been so many different versions of Doctor Who since then, but I sat down and said we need to get back to that 60s version, where Daleks were mysterious and powerful and had empires and things like that… It all became so nailed down when it went into colour. That's when the rules start to be fixed down. And the 60s were so mysterious and enigmatic, and the Doctor could have bits of dialogue like 'We've wandered into another universe…' And that would be impossible now. Fans would catalogue that out of existence now. You had such freedom.
R: Yes, The Web Planet! I love that one!
R: But it worked! I was born in 1963 and by the time I was about 5 or 6 the Zarbi were one of those names that kids mentioned as a classic! I was too young to remember them, but there were annuals with them in and things like that, and they were considered to be just brilliant monsters. No one at the time laughed! I think it was brave and brilliant!
Do you still feel like it's your baby, Verity?
V: No, I don't feel that in that way at all. I feel like I started off something that went on forever and ever, and has now been resuscitated in a new way and is very successful. But it's not mine any more. It has bits of my thing, but it's another entity, and that's jolly good. I do feel proud that years ago, knowing very little, I started something that is still running… Of course I do.


One of Aircraft Fasteners' primary insert and stud manufacturers is Acme Industrial Company.
Since 1914, Acme Industrial has been a major force in supplying precision steel products to the industrial and military sectors. Acme's many years of experience help it to provide the quality expected from a fastener manufacturer as evidenced by approvals from major worldwide aerospace manufacturers.
Acme threaded inserts come in sizes: Miniature, Lightweight, Heavy Duty and Extra Heavy Duty threaded insert types with Non-locking and Self-locking internal threads.
Inserts for specific uses are available in floating, blind end, solid and cast-in configurations.
We are authorized distributors for Acme products. Please contact us for assistance with your Acme product needs.


text:
- Any -BlogCollectionExhibitionFAQBasic pagePress ReleasePublic ArtVideo Art
Aviation Museum & Library
Support Affiliate
Public Art Map
Video Arts
Kids' Spot
Image Permissions
Main navigation (mobile)
Exhibitions/
Aviation Evolutions
Exhibition Image Gallery
Aviation Evolutions:
The Jim Lund 1:72 Scale Model Airplane Collection
Jim Lund, a Bay Area native, has a passionate interest in aviation dating back to his childhood when he first constructed aircraft models. Later in life, he returned to the practice and has dedicated much of his time to model building as a way to explore and experience the astonishingly rapid advancement of aviation since the first airplane. With a keen eye for detail, Lund's research includes careful study of the photographic record to assure that his models are accurately portrayed. Numerous models were constructed or modified from kits produced by manufacturers worldwide. In the many instances when no kit was available, Lund crafted the model parts from scratch based on manufacturers' plans using the "vacuform" process—a method that creates plastic parts from his hand-carved wood forms.
The 1:72 scale, with one inch equal to six feet, originated in the 1930s with popular aircraft model makers such as Skybirds and Frog. It appeals to the aircraft modeling community because of the ease with which nearly all aircraft types, from the smallest to the largest, can be constructed and displayed. This constant provides one-to-one size comparisons, and in large groupings it dramatically reveals the progress of aircraft design. Lund has created nearly 1,600 models in 1:72 scale representing historically significant aircraft from the 1903 Wright Flyer to today's airliners. They are constructed using plastic, wood, metal, wire, string, and epoxy, and detailed with paint and decals. This exhibition presents nearly three hundred models of pioneer, sport, and commercial aircraft that Jim Lund generously donated to the SFO Museum aviation collection.
Special thanks to Jim and Christiane Lund for their generosity and ongoing support in making this exhibition possible.
©2017 by the San Francisco Airport Commission. All rights reserved.
Sign up for announcements
Visit FlySFO
© San Francisco International Airport

redpajama_set_name: RedPajamaCommonCrawl